mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝¹ : CommSemiring R
inst✝ : DecidableEq ι
κ : ι → Type u_5
s : Finset ι
t : (i : ι) → Finset (κ i)
f : (i : ι) → κ i → R
⊢ ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih =>
    have h₁ : ∀ x ∈ t a, ∀ y ∈ t a, x ≠ y →
      Disjoint (image (Pi.cons s a x) (pi s t)) (image (Pi.cons s a y) (pi s t)) := by
      intro x _ y _ h
      simp only [disjoint_iff_ne, mem_image]
      rintro _ ⟨p₂, _, eq₂⟩ _ ⟨p₃, _, eq₃⟩ eq
      have : Pi.cons s a x p₂ a (mem_insert_self _ _)
              = Pi.cons s a y p₃ a (mem_insert_self _ _) := by rw [eq₂, eq₃, eq]
      rw [Pi.cons_same, Pi.cons_same] at this
      exact h this
    rw [prod_insert ha, pi_insert ha, ih, sum_mul, sum_biUnion h₁]
    refine sum_congr rfl fun b _ => ?_
    have h₂ : ∀ p₁ ∈ pi s t, ∀ p₂ ∈ pi s t, Pi.cons s a b p₁ = Pi.cons s a b p₂ → p₁ = p₂ :=
      fun p₁ _ p₂ _ eq => Pi.cons_injective ha eq
    rw [sum_image h₂, mul_sum]
    refine sum_congr rfl fun g _ => ?_
    rw [attach_insert, prod_insert, prod_image]
    · simp only [Pi.cons_same]
      congr with ⟨v, hv⟩
      congr
      exact (Pi.cons_ne (by rintro rfl; exact ha hv)).symm
    · exact fun _ _ _ _ => Subtype.ext ∘ Subtype.mk.inj
    · simpa only [mem_image, mem_attach, Subtype.mk.injEq, true_and,
        Subtype.exists, exists_prop, exists_eq_right] using ha

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
y : V
hyq : y ∈ q
hyp : y ∉ s
⊢ K ∙ x ⊔ s ≤ q

Tactic:
obtain ⟨c, z, hz, rfl⟩ : ∃ c : K, ∃ z ∈ s, c • x + z = y := by
    simpa [mem_sup, mem_span_singleton] using hqp.le hyq

Goal state after:
K : Type u_3
V : Type u_6
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : V
s q : Submodule K V
hpq : s < q
hqp : q < K ∙ x ⊔ s
c : K
z : V
hz : z ∈ s
hyq : c • x + z ∈ q
hyp : c • x + z ∉ s
⊢ K ∙ x ⊔ s ≤ q
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ {a} ∪ f.support = insert a f.support

pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint (single a b).support f.support

Tactic:
insert_eq

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ {a} ∪ f.support = {a} ∪ f.support

ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint (single a b).support f.support
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ {a} ∪ f.support = insert a f.support

pp: ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support

Tactic:
insert_eq

Goal state after:
ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ {a} ∪ f.support = {a} ∪ f.support

ι : Type u_1
M : Type u_3
inst✝ : AddZeroClass M
a : ι
b : M
f : ι →₀ M
ha : a ∉ f.support
hb : b ≠ 0
H : (single a b).support = {a}
⊢ Disjoint f.support (single a b).support
Module: Mathlib.Algebra.Group.Finsupp

Goal state before:
pp: case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ motive f

Tactic:
rw [← single_add_erase a f]

Goal state after:
case refine_2
ι : Type u_1
M : Type u_3
inst✝¹ : AddZeroClass M
inst✝ : LinearOrder ι
motive : (ι →₀ M) → Prop
f✝ : ι →₀ M
zero : motive 0
single_add : ∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (single a b + f)
s✝ : Finset ι
a : ι
s : Finset ι
hm : ∀ x ∈ s, x < a
hf : ∀ (f : ι →₀ M), f.support = s → motive f
f : ι →₀ M
hs : f.support = insert a s
hs' : (erase a f).support = s
⊢ motive (single a (f a) + erase a f)
Module: Mathlib.Data.Finsupp.Option

Goal state before:
pp: case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ optionElim 0 0 = 0

Tactic:
optionElim_zero,

Goal state after:
case mp
α : Type u_1
M : Type u_2
inst✝ : Zero M
⊢ single none 0 = 0
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ HasFiniteMulSupport (f ∘ g)

Tactic:
refine Set.Finite.of_injOn ?_ (Set.injOn_of_injective hg) hf

Goal state after:
α : Type u_1
M : Type u_2
inst✝ : One M
β : Type u_3
f : β → M
g : α → β
hg : Injective g
hf : HasFiniteMulSupport f
⊢ Set.MapsTo g (mulSupport (f ∘ g)) (mulSupport f)
Module: Mathlib.Algebra.FiniteSupport.Basic

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : One M
β : Type u_3
f : β → M
g : α → β
inst✝ : One β
hfg : HasFiniteMulSupport (f ∘ g)
h : f 1 = 1
hf : Injective f
⊢ HasFiniteMulSupport g

Tactic:
refine Set.Finite.subset hfg fun _ ha ↦ Set.mem_ofPred.mpr fun H ↦ Set.mem_ofPred.mp ha ?_
  grind

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
R✝ : Type u_3
S✝ : Type u_4
R : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : DecidablePred fun x ↦ x = 0
inst✝⁴ : NoZeroDivisors R
S : Type u_6
inst✝³ : Semiring S
inst✝² : PartialOrder S
inst✝¹ : IsOrderedRing S
inst✝ : Nontrivial S
x y : R
⊢ (if x + y = 0 then 0 else 1) ≤ (if x = 0 then 0 else 1) + if y = 0 then 0 else 1

Tactic:
by
    rcases eq_or_ne x 0 with rfl | hx
    · simp
    rcases eq_or_ne y 0 with rfl | hy
    · simp
    simp only [hx, ↓reduceIte, hy, one_add_one_eq_two]
    rcases eq_or_ne (x + y) 0 with hxy | hxy <;> simp [hxy, one_le_two]

Goal state after:
Module: Mathlib.Algebra.Order.AbsoluteValue.Basic

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : 1 < v y
hy₀ : y ≠ 0
⊢ ∃ x, x ≠ 0 ∧ v x < 1

Tactic:
refine ⟨y⁻¹, inv_ne_zero hy₀, ?_⟩

Goal state after:
R : Type u_3
S : Type u_4
inst✝⁴ : Field R
inst✝³ : Semifield S
inst✝² : LinearOrder S
inst✝¹ : IsStrictOrderedRing S
inst✝ : ExistsAddOfLE S
v : AbsoluteValue R S
h : v.IsNontrivial
y : R
hy : 1 < v y
hy₀ : y ≠ 0
⊢ v y⁻¹ < 1
Module: Mathlib.Algebra.Order.BigOperators.Group.Multiset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
hs_nonempty : s ≠ ∅
⊢ f s.prod ≤ (map f s).prod

Tactic:
induction s using Quotient.inductionOn with
  | h l => simp [l.le_prod_nonempty_of_submultiplicative f h_mul (by simpa using hs_nonempty)]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : CommMonoid α
inst✝² : CommMonoidWithZero β
inst✝¹ : PartialOrder β
inst✝ : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : (∀ (a : α), a ∈ s → p a) → f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : ¬s = ∅
hps : ∀ (x : α), x ∈ s → p x
hp_prod : p s.prod
⊢ f a * f s.prod ≤ f a * (map f s).prod

Tactic:
gcongr; exacts [h0 _, hs hps]

Goal state after:
Module: Mathlib.Data.Finsupp.Basic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst✝¹ : Zero γ
inst✝ : AddMonoid M
α : Type u_12
β : Type u_13
x✝ y✝ : α ⊕ β →₀ M
⊢ sumFinsuppEquivProdFinsupp.toFun (x✝ + y✝) = sumFinsuppEquivProdFinsupp.toFun x✝ + sumFinsuppEquivProdFinsupp.toFun y✝

Tactic:
ext <;>
        simp only [Equiv.toFun_as_coe, Prod.fst_add, Prod.snd_add, add_apply,
          snd_sumFinsuppEquivProdFinsupp, fst_sumFinsuppEquivProdFinsupp]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LSum

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
⊢ f ∘ₗ f.splittingOfFinsuppSurjective s = id

Tactic:
ext x
  dsimp [splittingOfFinsuppSurjective]
  congr
  rw [sum_single_index, one_smul]
  · exact (s (Finsupp.single x 1)).choose_spec
  · rw [zero_smul]

Goal state after:
Module: Mathlib.Order.Interval.Set.Fin

Goal state before:
pp: n : ℕ
i j : Fin n
⊢ val '' Ico i j = Ico ↑i ↑j

Tactic:
by
  rw [← preimage_val_Ico_val, image_preimage_eq_inter_range, range_val, inter_eq_left]
  exact fun k hk ↦ hk.2.trans j.is_lt

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_7
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
f g : α → M
hf : HasFiniteMulSupport f
hf₀ : ∀ (a : α), 0 ≤ f a
hg : HasFiniteMulSupport g
h : f ≤ g
⊢ ∏ᶠ (a : α), f a ≤ ∏ᶠ (a : α), g a

Tactic:
by
  have : Fintype ↑(f.mulSupport ∪ g.mulSupport) := (hf.union hg).fintype
  let s := (f.mulSupport ∪ g.mulSupport).toFinset
  rw [finprod_eq_finsetProd_of_mulSupport_subset f (show f.mulSupport ⊆ s by grind),
    finprod_eq_finsetProd_of_mulSupport_subset g (show g.mulSupport ⊆ s by grind)]
  exact Finset.prod_le_prod (fun i _ ↦ hf₀ i) fun i _ ↦ h i

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
⊢ x ∈ span R (v '' ↑s) ↔ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
← mem_span_range_iff_exists_fun,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : α → M
x : M
s : Finset α
⊢ x ∈ span R (v '' ↑s) ↔ x ∈ span R (Set.range fun i ↦ v ↑i)
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
x : M
s : Set α
inst✝ : Fintype ↑s
⊢ x ∈ span R (v '' s) ↔ ∃ c, ∑ i, c i • v ↑i = x

Tactic:
← mem_span_range_iff_exists_fun,

Goal state after:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
x : M
s : Set α
inst✝ : Fintype ↑s
⊢ x ∈ span R (v '' s) ↔ x ∈ span R (Set.range fun i ↦ v ↑i)
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
a : α
s : Set α
f : α → M
h : a ∉ s
hs : (s ∩ mulSupport f).Finite
⊢ ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = f a * ∏ᶠ (i : α) (_ : i ∈ s), f i

Tactic:
by
  rw [insert_eq, finprod_mem_union' _ _ hs, finprod_mem_singleton]
  · rwa [disjoint_singleton_left]
  · exact (finite_singleton a).inter_of_left _

Goal state after:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case neg
α : Type u
m n o : ℕ
ho : o + 1 = m + 1 + n
x : α
u : Fin m → α
v : Fin n → α
i : Fin (o + 1)
h : ¬↑i < m + 1
⊢ v ⟨↑i - (m + 1), ⋯⟩ = vecCons x (fun i ↦ if h : ↑i < m then u ⟨↑i, h⟩ else v ⟨↑i - m, ⋯⟩) i

Tactic:
· rcases i with ⟨⟨⟩ | i, hi⟩
    · simp at h
    · rw [not_lt, Fin.val_mk, Nat.add_le_add_iff_right] at h
      simp [not_lt.2 h]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ᶠ (i : α) (_ : i ∈ ↑s) (j : β) (_ : j ∈ ↑t), f i j = ∏ᶠ (j : β) (_ : j ∈ ↑t) (i : α) (_ : i ∈ ↑s), f i j

Tactic:
simp only [finprod_mem_coe_finset]

Goal state after:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α → β → M
s : Finset α
t : Finset β
⊢ ∏ i ∈ s, ∏ i_1 ∈ t, f i i_1 = ∏ i ∈ t, ∏ i_1 ∈ s, f i_1 i
Module: Mathlib.Algebra.Group.Fin.Basic

Goal state before:
pp: n✝ n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
⊢ ↑(⟨a, ha⟩ - ⟨b, hb⟩) = ↑(⟨a, ha⟩ + -⟨b, hb⟩)

Tactic:
by simp [Fin.sub_def, Fin.neg_def, Fin.add_def, Nat.add_comm]

Goal state after:
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inr.inl
y z : ℕ∞
⊢ 1 ^ (y + z) = 1 ^ y * 1 ^ z

Tactic:
simp only [one_epow, mul_one]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_2
ι : Type u'
R : Type u_2
K : Type u_3
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Semiring K
inst✝² : SMulWithZero R K
inst✝¹ : Module K M
inst✝ : IsScalarTower R K M
hinj : Injective fun r ↦ r • 1
li : LinearIndependent K v
x y : ι →₀ R
hxy : (Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) y
f : R → K := fun r ↦ r • 1
this : Finsupp.mapRange f ⋯ x = Finsupp.mapRange f ⋯ y
⊢ x = y

Tactic:
ext i
    exact hinj congr($this i)

Goal state after:
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: m n : ℕ
inst✝ : NeZero m
i : Fin n
j : Fin m
⊢ ↑(finFunctionFinEquiv (Pi.single i j)) = ↑j * m ^ ↑i

Tactic:
rw [finFunctionFinEquiv_apply, Fintype.sum_eq_single i, Pi.single_eq_same]
  rintro x hx
  rw [Pi.single_eq_of_ne hx, Fin.val_zero, zero_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Defs

Goal state before:
pp: case refine_2.specialize_1
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : LinearOrder R
inst✝² : CanonicallyOrderedAdd R
inst✝¹ : AddRightReflectLE R
inst✝ : IsCancelAdd M
this✝ : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t → ∑ i ∈ s, f i • v i = ∑ i ∈ t, f i • v i → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
s : Finset ι
f g : ι → R
heq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
⊢ ∀ ⦃a : ι⦄, a ∈ s ∧ g a ≤ f a → ¬(a ∈ s ∧ f a < g a)

Tactic:
exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'

Goal state after:
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ a % c + b % c < c * 2

Tactic:
rw [mul_two]

Goal state after:
a b c : ℕ
this : (a + b) % c = (a % c + b % c) % c
hc0 : ¬c = 0
h : c ≤ a % c + b % c
⊢ a % c + b % c < c + c
Module: Mathlib.LinearAlgebra.Dimension.Finrank

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ toNat (Module.rank R M) = toNat (Module.rank R N)

Tactic:
← Cardinal.toNat_lift,

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M ≃ₗ[R] N
⊢ toNat (lift.{?u.31, v} (Module.rank R M)) = toNat (Module.rank R N)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ Odd (insert a s).ncard ↔ Even s.ncard

Tactic:
rw [ncard_insert_of_notMem ha hs, Nat.odd_add]

Goal state after:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hs : s.Finite
⊢ (Odd s.ncard ↔ Even 1) ↔ Even s.ncard
Module: Mathlib.Algebra.Field.IsField

Goal state before:
pp: R : Type u
inst✝ : Ring R
hf : IsField R
x : R
hx : x ≠ 0
y z : R
hxy : x * y = 1
hxz : x * z = 1
⊢ y * (x * z) = x * y * z

Tactic:
rw [← mul_assoc, hf.mul_comm y x]

Goal state after:
Module: Mathlib.LinearAlgebra.Quotient.Basic

Goal state before:
pp: case mk
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
p : Submodule R M
R₂ : Type u_3
M₂ : Type u_4
inst✝³ : Ring R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : p ≤ f.ker
q : Submodule R (M ⧸ p)
w✝ : M ⧸ p
x : M
hxq : Quot.mk (⇑p.quotientRel) x ∈ ↑q
⊢ (p.liftQ f h) (Quot.mk (⇑p.quotientRel) x) ∈ map f (comap p.mkQ q)

Tactic:
exact ⟨x, hxq, rfl⟩

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f : ι → α
i : ι
⊢ (partialSups f) i = ⨆ j, ⨆ (_ : j ≤ i), f j

Tactic:
simpa only [iSup_subtype] using! partialSups_eq_ciSup_Iic f i

Goal state after:
Module: Mathlib.Order.Disjointed

Goal state before:
pp: case succ.inr.hab
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : PartialOrder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
n : ℕ
i : ι
hi : #(Iio i) ≤ n + 1
hn : #(Iio i) = n + 1
hun : (Iio i).biUnion Iic = Iio i
ih : ∀ (i : ι), #(Iio i) ≤ n → (Iic i).sup (disjointed f) = (Iic i).sup f
x : ι
hx : x ∈ Iio i
⊢ #(Iio x) < #(Iic x)

Tactic:
simpa only [Iic_eq_cons_Iio, card_cons] using Nat.lt_succ_self _

Goal state after:
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
⊢ {a ∈ antidiagonal n | k ≤ a.2} =
    map ((Embedding.refl ℕ).prodMap { toFun := fun x ↦ x + k, inj' := ⋯ }) (antidiagonal (n - k))

Tactic:
have aux₁ : fun a ↦ k ≤ a.snd = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
  have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔
                      ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
  rw [← map_prodComm_antidiagonal]
  simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h,
    map_map]
  ext ⟨i, j⟩
  simpa using aux₂ i j

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Semiring α
x y : α
⊢ span {x, y} = span {y, x}

Tactic:
by
  simp only [span_insert, sup_comm]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
x : α
⊢ span {x} = ⊤ ↔ IsUnit x

Tactic:
by
  rw [isUnit_iff_dvd_one, ← span_singleton_le_span_singleton, span_singleton_one, eq_top_iff]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : Ring α
x y x✝¹ : α
x✝ : ∃ a b, a * x + b * y = x✝¹
a b : α
h : a * x + b * y = x✝¹
⊢ a * (x + y) + (b - a) * y = x✝¹

Tactic:
rw [mul_add, sub_mul, add_add_sub_cancel, h]

Goal state after:
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) =
    ∑ i ∈ range (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i

Tactic:
rw [range_eq_Ico, sum_Ico_reflect _ _ (by lia)]

Goal state after:
m : ℕ
this : ∑ i ∈ range (m + 1), (2 * m + 1).choose (2 * m + 1 - i) = ∑ i ∈ range (m + 1), (2 * m + 1).choose i
⊢ ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i +
      ∑ j ∈ Ico (2 * m + 1 + 1 - (m + 1)) (2 * m + 1 + 1 - 0), (2 * m + 1).choose j =
    ∑ i ∈ Ico 0 (m + 1), (2 * m + 1).choose i + ∑ i ∈ Ico (m + 1) (2 * m + 2), (2 * m + 1).choose i
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x ∈ (LinearMap.toSpanSingleton R R e).ker ↔ x ∈ Ideal.span {1 - e}

Tactic:
by
  rw [Ideal.mem_span_singleton']
  refine ⟨fun h ↦ ⟨x, by rw [mul_sub, show x * e = 0 from h, mul_one, sub_zero]⟩, fun h ↦ ?_⟩
  obtain ⟨x, rfl⟩ := h
  change x * (1 - e) * e = 0
  rw [mul_assoc, sub_mul, one_mul, he, sub_self, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.IterateMapComap

Goal state before:
pp: case a
R : Type u_1
N : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f i : N →ₗ[R] M
K : Submodule R N
h : map f K ≤ map i K
n : ℕ
ih : map f (f.iterateMapComap i n K) ≤ map i (f.iterateMapComap i n K)
⊢ map f (f.iterateMapComap i n K) ≤ map i ((fun K ↦ comap f (map i K))^[n] K)

Tactic:
exact ih

Goal state after:
Module: Mathlib.Order.Filter.Bases.Basic

Goal state before:
pp: α : Type u_1
ι : Sort u_4
p : ι → Prop
s : ι → Set α
h : IsBasis p s
t : Set α
⊢ t ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ t

Tactic:
by simp only [h.mem_filter_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.Finsupp.Pi

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
⊢ x ∈ comap (lsingle i) (submodule p) ↔ x ∈ p i

Tactic:
refine ⟨fun hx ↦ by simpa using hx i, fun hx j ↦ ?_⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_5
p : α → Submodule R M
i : α
x : M
hx : x ∈ p i
j : α
⊢ ((lsingle i) x) j ∈ p j
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map ψ (map φ F) = map ρ (map θ F)

Tactic:
Filter.map_map,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
φ : α → β
θ : α → γ
ψ : β → δ
ρ : γ → δ
H : ψ ∘ φ = ρ ∘ θ
F : Filter α
⊢ map (ψ ∘ φ) F = map ρ (map θ F)
Module: Mathlib.Order.Filter.AtTopBot.Defs

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : α → Type u_6
inst✝² : Preorder ι
s : ι → Set α
inst✝¹ : (i : ι) → DecidablePred fun x ↦ x ∈ s i
inst✝ : DecidablePred fun x ↦ x ∈ ⋂ i, s i
hs : Antitone s
f g : (a : α) → β a
a : α
⊢ ∀ᶠ (i : ι) in atTop, (s i).piecewise f g a = (⋂ i, s i).piecewise f g a

Tactic:
classical
  convert! ← (compl_anti.comp hs).piecewise_eventually_eq_iUnion g f a using 3
  · convert! congr_fun (Set.piecewise_compl (s _) g f) a
  · simp only [(· ∘ ·), ← compl_iInter, Set.piecewise_compl]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
b : β
⊢ comap m (pure b) = 𝓟 (m ⁻¹' {b})

Tactic:
rw [← principal_singleton, comap_principal]

Goal state after:
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter β
m : α → β
⊢ map m (comap m f) = f ⊓ 𝓟 (range m)

Tactic:
refine le_antisymm (le_inf map_comap_le <| le_principal_iff.2 range_mem_map) ?_
  rintro t' ⟨t, ht, sub⟩
  refine mem_inf_principal.2 (mem_of_superset ht ?_)
  rintro _ hxt ⟨x, rfl⟩
  exact sub hxt

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Disjoint

Goal state before:
pp: case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint atBot atTop

Tactic:
refine disjoint_of_disjoint_of_mem ?_ (Iic_mem_atBot y) (Ici_mem_atTop x)

Goal state after:
case neg
α : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Nontrivial α
x y : α
hne : x ≠ y
hle : ¬x ≤ y
⊢ Disjoint (Iic y) (Ici x)
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ (l ⊓ 𝓟 {x | p x}).NeBot

Tactic:
neBot_iff,

Goal state after:
α : Type u
l : Filter α
p : α → Prop
⊢ (∃ᶠ (x : α) in l, p x) ↔ l ⊓ 𝓟 {x | p x} ≠ ⊥
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
m : α → β
⊢ map m f = ⊥ → f = ⊥

Tactic:
rw [← empty_mem_iff_bot, ← empty_mem_iff_bot]
    exact id

Goal state after: