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

Goal state before:
pp: α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Finset β
f : α → β → M
h : ∀ b ∈ s, HasFiniteMulSupport fun a ↦ f a b
⊢ ∏ᶠ (a : α), ∏ b ∈ s, f a b = ∏ b ∈ s, ∏ᶠ (a : α), f a b

Tactic:
by
  have hU :
    (mulSupport fun a => ∏ b ∈ s, f a b) ⊆
      (s.finite_toSet.biUnion fun b hb => h b (Finset.mem_coe.1 hb)).toFinset := by
    rw [Finite.coe_toFinset]
    intro x hx
    simp only [exists_prop, mem_iUnion, Ne, mem_mulSupport, Finset.mem_coe]
    contrapose! hx
    rw [mem_mulSupport, not_not, Finset.prod_congr rfl hx, Finset.prod_const_one]
  rw [finprod_eq_prod_of_mulSupport_subset _ hU, Finset.prod_comm]
  refine Finset.prod_congr rfl fun b hb => (finprod_eq_prod_of_mulSupport_subset _ ?_).symm
  intro a ha
  simp only [Finite.coe_toFinset, mem_iUnion]
  exact ⟨b, hb, ha⟩

Goal state after:
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
α : Type u_1
v : Fin n → α
a : α
⊢ snoc v a = fun i ↦ cons a v ((finRotate (n + 1)) i)

Tactic:
by
  ext ⟨i, h⟩
  by_cases h' : i < n
  · rw [finRotate_of_lt h', Fin.snoc, Fin.cons, dif_pos h']
    rfl
  · have h'' : n = i := by
      simp only [not_lt] at h'
      exact (Nat.eq_of_le_of_lt_succ h' h).symm
    subst h''
    rw [finRotate_last', Fin.snoc, Fin.cons, dif_neg (lt_irrefl _)]
    rfl

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Set.range ⇑(Finsupp.linearCombination R v) ⊆ ↑(Finsupp.linearCombination R v).range

Tactic:
LinearMap.coe_range

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn ⇑f ↑(span R (Set.range v))
⊢ Set.range ⇑(Finsupp.linearCombination R v) ⊆ Set.range ⇑(Finsupp.linearCombination R v)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ map (Finsupp.linearCombination R v) ⊥ ≤ ⊥

Tactic:
map_bot

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hv : Injective ⇑(f ∘ₗ Finsupp.linearCombination R v)
⊢ ⊥ ≤ ⊥
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + a ^ (c - b) - 1

Tactic:
← mul_add_one,

Goal state after:
case inr.inr.inr.inr
a b c : ℕ
ha0 : a > 0
ha1 : succ 0 < a
hb0 : b > 0
h : b ≤ c
⊢ a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1 + 1) - 1
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ (a * b).gcd (d * b) = b

Tactic:
gcd_mul_right

Goal state after:
a b d : ℕ
hac : a.Coprime (d * b)
b_dvd_c : b ∣ d * b
⊢ a.gcd d * b = b
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case inl
n : ℕ
G : Type u_3
inst✝ : Group G
g : Fin (n + 1) → G
j : Fin (n + 1)
k : Fin n
h : ↑k < ↑j
⊢ (partialProd g (j.succ.succAbove k.castSucc))⁻¹ * partialProd g (j.succAbove k).succ =
    j.contractNth (fun x1 x2 ↦ x1 * x2) g k

Tactic:
rwa [succAbove_of_castSucc_lt, succAbove_of_castSucc_lt, partialProd_right_inv,
    contractNth_apply_of_lt]
    · assumption
    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
      exact le_of_lt h

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s t : Set M
hs : LinearIndepOn R id s
h : t ⊆ s
hst : s ⊆ ↑(span R t)
⊢ s = t

Tactic:
let f : t ↪ s :=
    ⟨fun x => ⟨x.1, h x.2⟩, fun a b hab => Subtype.coe_injective (Subtype.mk.inj hab)⟩
  have h_surj : Surjective f := by
    apply surjective_of_linearIndependent_of_span hs f _
    convert! hst <;> simp [f, comp_def]
  change s = t
  apply Subset.antisymm _ h
  intro x hx
  rcases h_surj ⟨x, hx⟩ with ⟨y, hy⟩
  convert! y.mem
  rw [← Subtype.mk.inj hy]

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

Goal state before:
pp: m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ a ≡ b [MOD m / m.gcd c]

Tactic:
apply cancel_left_div_gcd hm

Goal state after:
m a b c : ℕ
hm : 0 < m
h : a * c ≡ b * c [MOD m]
⊢ c * a ≡ c * b [MOD m]
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∑ i, ↑(f i.castSucc) * ∏ j, n (Fin.castLE ⋯ j) + ↑(f (Fin.last m)) * ∏ j, n (Fin.castLE ⋯ j) <
    (∏ i, n i.castSucc) * n (Fin.last m)

Tactic:
suffices
        ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
          ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
            (∏ i : Fin m, n i) * nn by
        solve_by_elim

Goal state after:
case succ
ι : Type u_1
M : Type u_2
m : ℕ
ih : ∀ {n : Fin m → ℕ} (f : (i : Fin m) → Fin (n i)), ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) < ∏ i, n i
n : Fin (m + 1) → ℕ
f : (i : Fin (m + 1)) → Fin (n i)
⊢ ∀ (n : Fin m → ℕ) (nn : ℕ) (f : (i : Fin m) → Fin (n i)) (fn : Fin nn),
    ∑ i, ↑(f i) * ∏ j, n (Fin.castLE ⋯ j) + ↑fn * ∏ j, n j < (∏ i, n i) * nn
Module: Mathlib.Data.ZMod.Defs

Goal state before:
pp: case isFalse
n : ℕ
inst✝ : NeZero n
x : ℤ
h : ¬0 ≤ x
⊢ ↑(-↑x.natAbs) = (x % ↑n).toNat

Tactic:
· simp only [Fin.val_neg, Fin.natCast_eq_zero, Fin.val_natCast]
    split <;> rename_i h
    · rw [← Int.natCast_dvd] at h
      rw [Int.emod_eq_zero_of_dvd h, Int.toNat_zero]
    · rw [Int.emod_natAbs_of_neg (by lia) (NeZero.ne n),
        if_neg (by rwa [← Int.natCast_dvd] at h)]
      have : x % n < n := Int.emod_lt_of_pos x (by have := NeZero.ne n; lia)
      lia

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: α : Type u_1
inst✝ : Subsingleton α
⊢ card α ≤ 1

Tactic:
simpa [card_le_one_iff_subsingleton]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ card (α → β) = card β ^ ⊤

Tactic:
rw [b_1, one_epow]

Goal state after:
case inr.inr.inr.inl
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ card (α → β) = 1
Module: Mathlib.SetTheory.Cardinal.Finite

Goal state before:
pp: case inr.inr.inr.inl.a
α : Type u_3
β : Type u_4
α_emp : Nonempty α
h✝ : Infinite α
b_1 : card β = 1
⊢ card (α → β) ≤ 1

Tactic:
let := (card_le_one_iff_subsingleton β).1 b_1.le
        exact (card_le_one_iff_subsingleton (α → β)).2 Pi.instSubsingleton

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ 1 ≤ s.encard ↔ s.Nonempty

Tactic:
by
  rw [nonempty_iff_ne_empty, Ne, ← encard_eq_zero, Order.one_le_iff_ne_zero]

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a (s \ {b})).encard = s.encard

Tactic:
by
  rw [encard_insert_of_notMem, encard_sdiff_singleton_add_one hb]
  simp_all only [mem_sdiff, mem_singleton_iff, false_and, not_false_eq_true]

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

Goal state before:
pp: case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ Finsupp.single i (l i) - l ∈ Finsupp.supported R R (univ \ {i})

Tactic:
rw [Finsupp.mem_supported']

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), a • v i ∈ span R (v '' (univ \ {i})) → a = 0
l : ι →₀ R
hl : (Finsupp.linearCombination R v) l = 0
i : ι
hn : ¬l i = 0
⊢ ∀ x ∉ univ \ {i}, (Finsupp.single i (l i) - l) x = 0
Module: Mathlib.SetTheory.Cardinal.NatCard

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Finite α
n : ℕ
h : Nat.card α = n
⊢ α ≃ Fin n

Tactic:
by
  subst h
  apply Finite.equivFin

Goal state after:
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
k : ℕ
⊢ s.encard ≤ ↑k ↔ s.Finite ∧ s.ncard ≤ k

Tactic:
by
  rw [encard_le_coe_iff, and_congr_right_iff]
  exact fun hfin ↦ ⟨fun ⟨n₀, hn₀, hle⟩ ↦ by rwa [ncard_def, hn₀, ENat.toNat_natCast],
    fun h ↦ ⟨s.ncard, by rw [hfin.cast_ncard_eq], h⟩⟩

Goal state after:
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑(Quotient.out ↑a.2 * ↑a.1) ∈ t

Tactic:
mk_mul_of_mem _ a.1.2,

Goal state after:
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × ↑t
⊢ ↑(Quotient.out ↑a.2) ∈ t
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
s : Set α
⊢ sᶜ.ncard = 0 ↔ s.ncard = Nat.card α

Tactic:
← ncard_add_ncard_compl s,

Goal state after:
α : Type u_1
inst✝ : Finite α
s : Set α
⊢ sᶜ.ncard = 0 ↔ s.ncard = s.ncard + sᶜ.ncard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Finite α
h : Nat.card α < s.ncard + t.ncard
⊢ (s ∩ t).Nonempty

Tactic:
rw [← ncard_union_add_ncard_inter s t] at h

Goal state after:
α : Type u_1
s t : Set α
inst✝ : Finite α
h : Nat.card α < (s ∪ t).ncard + (s ∩ t).ncard
⊢ (s ∩ t).Nonempty
Module: Mathlib.GroupTheory.QuotientGroup.Basic

Goal state before:
pp: ι : Type u_1
A : ι → Type u_2
inst✝ : (i : ι) → CommGroup (A i)
n : ℕ
⊢ (fun x ↦ ↑(1 x)) = 1

Tactic:
simp [Pi.one_def]

Goal state after:
Module: Mathlib.RingTheory.Congruence.Basic

Goal state before:
pp: R : Type u_3
inst✝¹ : Add R
inst✝ : Mul R
S : Set (RingCon R)
x y : R
h : (sInf S).toSetoid x y
r : Setoid R
x✝ : r ∈ (fun x ↦ x.toSetoid) '' S
c : RingCon R
hS : c ∈ S
hr : (fun x ↦ x.toSetoid) c = r
⊢ r x y

Tactic:
by rw [← hr]; exact h c hS

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (pred a) (Ico a b) = Ico (pred a) b

Tactic:
by
  ext x; simp +contextual [or_and_left, pred_le_iff_eq_or_le, pred_lt_of_le_of_not_isMin h ha]

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
⊢ comap (fst R M M₂) p = p.prod ⊤

Tactic:
ext ⟨x, y⟩; simp

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
q : Submodule R M₂
⊢ comap (snd R M M₂) q = ⊤.prod q

Tactic:
ext ⟨x, y⟩; simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : 0 ∘ₛₗ f = 0
⊢ f.range.mkQ.ker = ⊤

Tactic:
← h 0 (range f).mkQ (Eq.trans h₁ (range_mkQ_comp _).symm)

Goal state after:
R : Type u_1
M : Type u_2
R₂ : Type u_3
M₂ : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : M₂ →ₗ[R₂] M₂ ⧸ f.range), u ∘ₛₗ f = v ∘ₛₗ f → u = v
h₁ : 0 ∘ₛₗ f = 0
⊢ ker 0 = ⊤
Module: Mathlib.Data.Fintype.Order

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : Finite ι
inst✝² : Nonempty α
inst✝¹ : Preorder α
inst✝ : IsCodirectedOrder α
f : ι → α
⊢ BddBelow (Set.range f)

Tactic:
obtain ⟨M, hM⟩ := Finite.exists_ge f
  refine ⟨M, fun a ha => ?_⟩
  obtain ⟨b, rfl⟩ := ha
  exact hM b

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ ↑p₁
h2 : (x1, x2).2 ∈ ↑p₂
h1' : (inl R M M₂) x1 ∈ q
⊢ (inr R M M₂) x2 ∈ q

Tactic:
apply hK

Goal state after:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p₁ : Submodule R M
p₂ : Submodule R M₂
q : Submodule R (M × M₂)
hH : map (inl R M M₂) p₁ ≤ q
hK : map (inr R M M₂) p₂ ≤ q
x1 : M
x2 : M₂
h1 : (x1, x2).1 ∈ ↑p₁
h2 : (x1, x2).2 ∈ ↑p₂
h1' : (inl R M M₂) x1 ∈ q
⊢ (inr R M M₂) x2 ∈ map (inr R M M₂) p₂
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : PredOrder ι
inst✝ : IsSuccArchimedean ι
i j : ι
hij : i ≤ j
⊢ ∃ n, pred^[n] j = i

Tactic:
have h_exists := exists_succ_iterate_of_le hij
    obtain ⟨n, hn_eq, hn_lt_ne⟩ : ∃ n, succ^[n] i = j ∧ ∀ m < n, succ^[m] i ≠ j :=
      ⟨Nat.find h_exists, Nat.find_spec h_exists, fun m hmn ↦ Nat.find_min h_exists hmn⟩
    refine ⟨n, ?_⟩
    rw [← hn_eq]
    cases n with
    | zero => simp only [Function.iterate_zero, id]
    | succ n =>
      rw [pred_succ_iterate_of_not_isMax]
      rw [Nat.succ_sub_succ_eq_sub, tsub_zero]
      suffices succ^[n] i < succ^[n.succ] i from not_isMax_of_lt this
      refine lt_of_le_of_ne ?_ ?_
      · rw [Function.iterate_succ_apply']
        exact le_succ _
      · rw [hn_eq]
        exact hn_lt_ne _ (Nat.lt_succ_self n)

Goal state after:
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
⊢ False

Tactic:
obtain ⟨n, m, hnm, h_eq⟩ : ∃ n m, n < m ∧ succ^[n] i = succ^[m] i := by
      let f : ℕ → Finset.Icc i j := fun n ↦ ⟨succ^[n] i, h_mem n⟩
      obtain ⟨n, m, hnm_ne, hfnm⟩ : ∃ n m, n ≠ m ∧ f n = f m :=
        Finite.exists_ne_map_eq_of_infinite f
      have hnm_eq : succ^[n] i = succ^[m] i := by simpa only [f, Subtype.mk_eq_mk] using hfnm
      rcases le_total n m with h_le | h_le
      · exact ⟨n, m, lt_of_le_of_ne h_le hnm_ne, hnm_eq⟩
      · exact ⟨m, n, lt_of_le_of_ne h_le hnm_ne.symm, hnm_eq.symm⟩

Goal state after:
case inl
ι : Type u_1
inst✝² : LinearOrder ι
inst✝¹ : LocallyFiniteOrder ι
inst✝ : SuccOrder ι
i j : ι
hij : i < j
h : ∀ (n : ℕ), succ^[n] i ≠ j
h_lt : ∀ (n : ℕ), succ^[n] i < j
h_mem : ∀ (n : ℕ), succ^[n] i ∈ Finset.Icc i j
n m : ℕ
hnm : n < m
h_eq : succ^[n] i = succ^[m] i
⊢ False
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case refine_1
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≤ 0

pp: case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0

Tactic:
· rw [toZ_of_lt hi]
    lia

Goal state after:
case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : SuccOrder ι
inst✝¹ : IsSuccArchimedean ι
inst✝ : PredOrder ι
i0 i : ι
hi : i < i0
⊢ toZ i0 i ≠ 0
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
⊢ (a, b) ∈ {x ∈ antidiagonal n | x.1 = m} ↔ (a, b) ∈ if m ≤ n then {(m, n - m)} else ∅

Tactic:
suffices a = m → (a + b = n ↔ m ≤ n ∧ b = n - m) by
    rw [mem_filter, mem_antidiagonal, apply_ite (fun n ↦ (a, b) ∈ n), mem_singleton,
      Prod.mk_inj, ite_prop_iff_or]
    simpa [← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]

Goal state after:
A : Type u_1
inst✝⁸ : AddCommMonoid A
inst✝⁷ : PartialOrder A
inst✝⁶ : CanonicallyOrderedAdd A
inst✝⁵ : Sub A
inst✝⁴ : OrderedSub A
inst✝³ : AddLeftReflectLE A
inst✝² : HasAntidiagonal A
n m : A
inst✝¹ : DecidablePred fun x ↦ x = m
inst✝ : Decidable (m ≤ n)
a b : A
⊢ a = m → (a + b = n ↔ m ≤ n ∧ b = n - m)
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: A : Type u_1
inst✝¹ : Monoid A
inst✝ : HasMulAntidiagonal A
⊢ LeftInverse (fun x ↦ ⟨x.1 * x.2, ⟨x, ⋯⟩⟩) fun x ↦ ↑x.snd

Tactic:
by
    rintro ⟨n, ⟨k, l⟩, h⟩
    rw [mem_mulAntidiagonal] at h
    exact Sigma.subtype_ext h rfl

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

Goal state before:
pp: n : ℕ
⊢ (map (fun i ↦ (i, n - i)) (range (n + 1))).length = n + 1

Tactic:
length_map,

Goal state after:
n : ℕ
⊢ (range (n + 1)).length = n + 1
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hx : x ∈ I
h : y * x = 1
z : α
x✝ : z ∈ ⊤
⊢ z * (y * x) = z

Tactic:
by rw [h, mul_one]

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

Goal state before:
pp: α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = (a - b) * c + b * (c - d)

Tactic:
sub_mul,

Goal state after:
α : Type u
inst✝¹ : Ring α
I : Ideal α
a b c d : α
inst✝ : I.IsTwoSided
h1 : a - b ∈ I
h2 : c - d ∈ I
⊢ a * c - b * d = a * c - b * c + b * (c - d)
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 - a - (1 - a) * a = 1 - a

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 - a - (1 * a - a * a) = 1 - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ (1 - a) * a = 0

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
h : IsIdempotentElem a
⊢ 1 * a - a * a = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ (1 - a) * a = 0

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝ : NonAssocRing R
a : R
⊢ IsIdempotentElem a ↔ 1 * a - a * a = 0
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ (b - a) * (b - a) = b - a

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
a b : R
ha : IsIdempotentElem a
hb : IsIdempotentElem b
hab : a * b = a
hba : b * a = a
⊢ b * (b - a) - a * (b - a) = b - a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : (q - p) * q - (q - p) * p = q - p
⊢ Commute p q

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : q * q - p * q - (q * p - p * p) = q - p
⊢ Commute p q
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h2 : (p * q + q * p - p) * q = p * q
h1 : q * p * q = q * p
⊢ Commute p q

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsIdempotentElem p
hq : IsIdempotentElem q
h : p * (q - p) + (q - p) * p = 0
hqp : p * q + q * p - p = p
h1 : q * p * q = q * p
h2 : (p * q + q * p) * q - p * q = p * q
⊢ Commute p q
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ ∃ y, ∃ i ∈ I, y * x + i = 1

Tactic:
refine ⟨y, z, ?_, hy.symm⟩

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
hI : I.IsMaximal
x : α
hx : x ∉ I
H₁ : 1 ∉ I
H₂ : ∀ (J : Ideal α) (x : α), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
y z : α
hz : z ∈ span ↑I
hy : 1 = y * x + z
⊢ z ∈ I
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
⊢ y ∈ I

Tactic:
let J : Ideal α := Submodule.span α (insert x ↑I)

Goal state after:
α : Type u
inst✝ : CommSemiring α
I : Ideal α
H : I.IsMaximal
x y : α
hxy : x * y ∈ I
hx : x ∉ I
J : Ideal α := Submodule.span α (insert x ↑I)
⊢ y ∈ I
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 + a * y + (b - a) * y = x✝¹

Tactic:
sub_mul,

Goal state after:
α : 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 + a * y + (b * y - a * y) = x✝¹
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * ((1 - e) * e) = 0

Tactic:
sub_mul,

Goal state after:
R : Type u_1
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
x : R
⊢ x * (1 * e - e * e) = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
I✝ J : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
inst✝ : I.IsTwoSided
a₁ b₁ a₂ b₂ : R
h₁ : (QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid a₁ b₁
h₂ : (QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid a₂ b₂
⊢ (QuotientAddGroup.con (Submodule.toAddSubgroup I)).toSetoid (a₁ * a₂) (b₁ * b₂)

Tactic:
rw [Submodule.quotientRel_def] at h₁ h₂ ⊢

Goal state after:
R : Type u
inst✝¹ : Ring R
I✝ J : Ideal R
a b : R
S : Type v
x y : R
I : Ideal R
inst✝ : I.IsTwoSided
a₁ b₁ a₂ b₂ : R
h₁ : a₁ - b₁ ∈ I
h₂ : a₂ - b₂ ∈ I
⊢ a₁ * a₂ - b₁ * b₂ ∈ I
Module: Mathlib.Data.Nat.Choose.Sum

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∑ m ∈ x.powerset, f #m = ∑ m ∈ range (#x + 1), ∑ j ∈ x.powerset with #j = m, f #j

Tactic:
refine (sum_fiberwise_of_maps_to ?_ _).symm

Goal state after:
α : Type u_2
β : Type u_3
inst✝ : AddCommMonoid α
f : ℕ → α
x : Finset β
⊢ ∀ i ∈ x.powerset, #i ∈ range (#x + 1)
Module: Mathlib.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit.refine_2
α : Type u
inst✝ : CommSemiring α
a : α
max : (span {a}).IsMaximal
idem : ∀ (x : α), span {a} = span {x} → ¬IsIdempotentElem x
c d : α
ha : a = a * c * (a * d)
huv : ¬IsUnit (a * c) ∧ ¬IsUnit (a * d)
⊢ IsIdempotentElem (a * (c * d))

Tactic:
· rw [isIdempotentElem_iff]
      refine Eq.trans ?_ (congrArg (· * (c * d)) ha.symm)
      ring

Goal state after: