mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: case inr.inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k

Tactic:
have hk : k = Fin.succ ⟨k - 1, by lia⟩ := by grind

Goal state after:
case inr.inr.inr
α : Type u
n : ℕ
a : α
x : Fin n → α
i j : Fin n
k : Fin n.succ
hk₀ : k ≠ 0
hki : k ≠ i.succ
hkj : k ≠ j.succ
hk : k = ⟨↑k - 1, ⋯⟩.succ
⊢ vecCons a (x ∘ ⇑(Equiv.swap i j)) k = (vecCons a x ∘ ⇑(Equiv.swap i.succ j.succ)) k
Module: Mathlib.Logic.Equiv.Fin.Rotate

Goal state before:
pp: n : ℕ
i : Fin n.succ
⊢ i = i - 1 + 1

Tactic:
sub_add_cancel

Goal state after:
n : ℕ
i : Fin n.succ
⊢ i = i
Module: Mathlib.Algebra.BigOperators.Finprod

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
s : Multiset α
f : α → M
⊢ ∏ m ∈ s.toFinset, f m ^ count m s = ∏ᶠ (a : α), f a ^ count a s

Tactic:
eq_comm

Goal state after:
α : Type u_1
M : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommMonoid M
s : Multiset α
f : α → M
⊢ ∏ᶠ (a : α), f a ^ count a s = ∏ m ∈ s.toFinset, f m ^ count m s
Module: Mathlib.LinearAlgebra.Basis.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x y : M
hli : LinearIndependent R v
⊢ ⊤ ≤ span R (range fun i ↦ ⟨v i, ⋯⟩)

Tactic:
intro x _

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
v : ι → M
x✝ y : M
hli : LinearIndependent R v
x : ↥(span R (range v))
a✝ : x ∈ ⊤
⊢ x ∈ span R (range fun i ↦ ⟨v i, ⋯⟩)
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case inl
x y : ℕ∞
h : x ^ y = 1
y_0 : ¬y = 0
x_0 : x < 1
⊢ x = 1

Tactic:
rw [Order.lt_one_iff.1 x_0, zero_epow y_0] at h; contradiction

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i

Tactic:
by
      convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
      exact (if_pos hi).symm

Goal state after:
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: m n : ℕ
⊢ m.Coprime (m + n) ↔ m.Coprime n

Tactic:
add_comm,

Goal state after:
m n : ℕ
⊢ m.Coprime (n + m) ↔ m.Coprime n
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
⊢ a + b ≡ b [MOD n] ↔ n ∣ a

Tactic:
add_comm,

Goal state after:
n a b : ℕ
⊢ b + a ≡ b [MOD n] ↔ n ∣ a
Module: Mathlib.Algebra.BigOperators.Fin

Goal state before:
pp: case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ (1 + n✝) * (n✝ + 1) ^ n = (n✝ + 1) ^ (n + 1)

Tactic:
add_comm,

Goal state after:
case succ.succ
ι : Type u_1
M : Type u_2
n n✝ : ℕ
ih : ∀ (f : Fin n → Fin (n✝ + 1)), ∑ i, ↑(f i) * (n✝ + 1) ^ ↑i < (n✝ + 1) ^ n
f : Fin (n + 1) → Fin (n✝ + 1)
⊢ (n✝ + 1) * (n✝ + 1) ^ n = (n✝ + 1) ^ (n + 1)
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b : ℕ
⊢ n + a ≡ b [MOD n] ↔ a ≡ b [MOD n]

Tactic:
add_comm,

Goal state after:
n a b : ℕ
⊢ a + n ≡ b [MOD n] ↔ a ≡ b [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ b * n + a ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
add_comm,

Goal state after:
n a b c : ℕ
⊢ a + b * n ≡ c [MOD n] ↔ a ≡ c [MOD n]
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
⊢ ∃ a, f a = i

Tactic:
rcases Finsupp.single_of_embDomain_single (repr ⟨v i, _⟩) f i (1 : R) zero_ne_one.symm l_eq with
    ⟨i', hi'⟩

Goal state after:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
f : ι' ↪ ι
hss : range v ⊆ ↑(span R (range (v ∘ ⇑f)))
i : ι
repr : ↥(span R (range (v ∘ ⇑f))) → ι' →₀ R := ⇑⋯.repr
l : ι →₀ R := Finsupp.mapDomain (⇑f) (repr ⟨v i, ⋯⟩)
h_total_l : (Finsupp.linearCombination R v) l = v i
h_total_eq : (Finsupp.linearCombination R v) l = (Finsupp.linearCombination R v) (Finsupp.single i 1)
l_eq : Finsupp.embDomain f (repr ⟨v i, ⋯⟩) = Finsupp.single i 1
i' : ι'
hi' : repr ⟨v i, ⋯⟩ = Finsupp.single i' 1 ∧ f i' = i
⊢ ∃ a, f a = i
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ a ≡ b * n + c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
add_comm,

Goal state after:
n a b c : ℕ
⊢ a ≡ c + b * n [MOD n] ↔ a ≡ c [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ n * b + a ≡ c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
add_comm,

Goal state after:
n a b c : ℕ
⊢ a + n * b ≡ c [MOD n] ↔ a ≡ c [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: n a b c : ℕ
⊢ a ≡ n * b + c [MOD n] ↔ a ≡ c [MOD n]

Tactic:
add_comm,

Goal state after:
n a b c : ℕ
⊢ a ≡ c + n * b [MOD n] ↔ a ≡ c [MOD n]
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑n * n.gcdA m * ↑b + ↑(n.gcd m) * ↑a - ↑n * n.gcdA m * ↑a) / ↑(n.gcd m)

Tactic:
add_comm,

Goal state after:
case left.refine_1
m n a b c d : ℕ
h : a ≡ b [MOD n.gcd m]
hn : ¬n = 0
hm : ¬m = 0
hnonzero : ↑(n.gcd m) ≠ 0
hcoedvd : ∀ (t : ℤ), ↑(n.gcd m) ∣ t * (↑b - ↑a)
this : ↑(n.gcd m) - ↑n * n.gcdA m = ↑m * n.gcdB m
⊢ ↑n ∣ ↑a - (↑(n.gcd m) * ↑a + ↑n * n.gcdA m * ↑b - ↑n * n.gcdA m * ↑a) / ↑(n.gcd m)
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: case refine_1
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), ∑ i ∈ s, g i • (v ∘ Sum.inl) i = 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), ∑ i ∈ s, g i • (v ∘ Sum.inr) i = 0 → ∀ i ∈ s, g i = 0
hlr : ∀ x ∈ span R (v '' range Sum.inl), ∀ y ∈ span R (v '' range Sum.inr), x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : ∑ i ∈ s, g i • v i = 0
i✝ : ι ⊕ ι'
hi : i✝ ∈ s
this :
  ∑ i ∈ s.preimage Sum.inl ⋯, (fun x ↦ g x • v x) (Sum.inl i) =
    -∑ i ∈ s.preimage Sum.inr ⋯, (fun x ↦ g x • v x) (Sum.inr i)
i : ι
x✝ : i ∈ s.preimage Sum.inl ⋯
⊢ (fun x ↦ g x • v x) (Sum.inl i) ∈ span R (v '' range Sum.inl)

Tactic:
exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)

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

Goal state before:
pp: a b c : ℕ
hca : c ∣ b
⊢ (a + b) / c = a / c + b / c

Tactic:
add_comm,

Goal state after:
a b c : ℕ
hca : c ∣ b
⊢ (b + a) / c = a / c + b / c
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = t.encard - s.encard

Tactic:
← @Set.encard_sdiff_add_encard_of_subset _ s t h

Goal state after:
α : Type u_1
s t : Set α
h : s ⊆ t
hs : s.Finite
⊢ (t \ s).encard = (t \ s).encard + s.encard - s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑n + ↑1 ≤ ↑n
⊢ False

Tactic:
← Nat.cast_add,

Goal state after:
α : Type u_1
n : ℕ
t₀ : Set α
ht₀ : t₀.encard = ↑n
IH : ↑n ≤ t₀.encard → ∃ t ⊆ t₀, t.encard = ↑n
ht₀s : t₀ ⊆ t₀
hk : ↑(n + 1) ≤ ↑n
⊢ False
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).ncard = s.card

Tactic:
ncard_eq_toFinset_card _,

Goal state after:
α : Type u_1
s : Finset α
⊢ ⋯.toFinset.card = s.card
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Set β
H : Function.Injective f
hs : s ⊆ range f
⊢ (f ⁻¹' s).ncard = s.ncard

Tactic:
rw [← ncard_image_of_injective _ H, image_preimage_eq_iff.mpr hs]

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

Goal state before:
pp: α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∩ t).ncard + (s ∪ t).ncard = s.ncard + t.ncard

Tactic:
add_comm,

Goal state after:
α : Type u_1
s t : Set α
hs : s.Finite
ht : t.Finite
⊢ (s ∪ t).ncard + (s ∩ t).ncard = s.ncard + t.ncard
Module: Mathlib.GroupTheory.Coset.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f x✝ = f a ↔ f a = f x✝

Tactic:
eq_comm

Goal state after:
α : Type u_1
inst✝¹ : Group α
H : Type u_2
inst✝ : Group H
f : α →* H
a x✝ : α
⊢ f a = f x✝ ↔ f a = f x✝
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ sᶜ.ncard + s.ncard = Nat.card α

Tactic:
add_comm,

Goal state after:
α : Type u_1
s : Set α
hs : s.Finite
hsc : sᶜ.Finite
⊢ s.ncard + sᶜ.ncard = Nat.card α
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
⊢ (∃ a, s = {a}) → s.ncard = 1

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
α : Type u_1
a : α
⊢ {a}.ncard = 1
Module: Mathlib.LinearAlgebra.Quotient.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
r : R
x✝ y✝ : M
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
p p' : Submodule R M
S : Type u_3
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
P : Submodule R M
a : S
x y : M
h : P.quotientRel x y
⊢ -(a • x) + a • y ∈ P.toAddSubgroup

Tactic:
simpa using Submodule.smul_mem P (a • (1 : R)) (leftRel_apply.mp h)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (succ a) b) = Icc a b

Tactic:
by
  ext x; simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]; aesop

Goal state after:
Module: Mathlib.Order.PartialSups

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : SemilatticeSup α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ p ((partialSups f) i) ↔ ∀ j ≤ i, p (f j)

Tactic:
by
  rw [partialSups_apply, apply_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
c : R
x : M × M₂
hx : x.2 = f x.1
⊢ c • x ∈ {p | p.2 = f p.1}

Tactic:
change _ • _ = f (_ • _)

Goal state after:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
M₅ : Type u_1
M₆ : Type u_2
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommGroup M₃
inst✝⁴ : AddCommGroup M₄
inst✝³ : Module R M
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Module R M₄
f : M →ₗ[R] M₂
g : M₃ →ₗ[R] M₄
c : R
x : M × M₂
hx : x.2 = f x.1
⊢ c • x.2 = f (c • x.1)
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x.2 = g x.1 ↔ -g x.1 + x.2 = 0

Tactic:
add_comm,

Goal state after:
R : Type u
M₃ : Type y
M₄ : Type z
inst✝⁴ : Semiring R
inst✝³ : AddCommGroup M₃
inst✝² : AddCommGroup M₄
inst✝¹ : Module R M₃
inst✝ : Module R M₄
g : M₃ →ₗ[R] M₄
x : M₃ × M₄
⊢ x.2 = g x.1 ↔ x.2 + -g x.1 = 0
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ Icc a b, f x

Tactic:
Icc_eq_cons_Ioc h,

Goal state after:
α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a ≤ b
⊢ f a * ∏ x ∈ Ioc a b, f x = ∏ x ∈ cons a (Ioc a b) ⋯, f x
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝¹ : LinearOrder ι
inst✝ : LocallyFiniteOrder ι
i : ι
hi : succFn i ≤ i
j : ι
x✝ : i ≤ j
hij_lt : i < j
h_succFn_eq : succFn i = i
h_glb : IsGLB (↑(Finset.Ioc i j)) i
⊢ (Finset.Ioc i j).Nonempty

Tactic:
exact ⟨_, Finset.mem_Ioc.mpr ⟨hij_lt, le_rfl⟩⟩

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝² : CommMonoid M
f : α → M
a b : α
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
h : a < b
⊢ (∏ x ∈ Ioo a b, f x) * f b = ∏ x ∈ Ioc a b, f x

Tactic:
rw [mul_comm, mul_prod_Ioo_eq_prod_Ioc h]

Goal state after:
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: case h
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : kl.1 * kl.2 = n
⊢ n = kl.1 * kl.2

Tactic:
eq_comm

Goal state after:
case h
A : Type u_1
inst✝³ : CommMonoid A
inst✝² : PartialOrder A
inst✝¹ : CanonicallyOrderedMul A
inst✝ : HasMulAntidiagonal A
n : A
kl : A × A
hlk : n = kl.1 * kl.2
⊢ n = kl.1 * kl.2
Module: Mathlib.Algebra.Order.Antidiag.Prod

Goal state before:
pp: case mpr
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 a b : A
inst✝¹ : DecidablePred fun x ↦ x = a
inst✝ : Decidable (a ≤ n)
⊢ a ≤ n ∧ b = n - a → a + b = n

Tactic:
rintro ⟨h, rfl⟩
    exact add_tsub_cancel_of_le h

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

Goal state before:
pp: M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ j ∈ range n, f (n - 1 - j) = ∏ j ∈ range n, f j

Tactic:
cases n
  · simp
  · simp only [← Nat.Ico_zero_eq_range, Nat.succ_sub_succ_eq_sub, tsub_zero]
    rw [prod_Ico_reflect _ _ le_rfl]
    simp

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

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : OrderBot ι
inst✝ : OrderTop ι
⊢ ∀ {a b : ι},
    { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := fun i ↦ ⟨(toZ ⊥ i).toNat, ⋯⟩, invFun := fun n ↦ succ^[↑n] ⊥, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
intro i j
    simp only [Equiv.coe_fn_mk, Subtype.mk_le_mk, Int.toNat_le]
    rw [← toZ_le_toZ (i0 := (⊥ : ι)), Int.toNat_of_nonneg (toZ_nonneg bot_le)]

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

Goal state before:
pp: case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ k - j + (n - k) = i

Tactic:
add_comm,

Goal state after:
case refine_1
n k : ℕ
h : k ≤ n
i j : ℕ
hi : i + j = n ∧ j ≤ k
⊢ n - k + (k - j) = i
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ l + (n - k + j) = n

Tactic:
add_comm,

Goal state after:
case refine_2
n k : ℕ
h : k ≤ n
j l : ℕ
hl : l + j = k
⊢ n - k + j + l = n
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
⊢ x ∈ I

Tactic:
have := I.mul_mem_left y' h

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
x y : α
hy : IsUnit y
h : y * x ∈ I
y' : α
hy' : y' * y = 1
this : y' * (y * x) ∈ I
⊢ x ∈ I
Module: Mathlib.RingTheory.Ideal.Defs

Goal state before:
pp: α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (m + (n - m)) ∈ I

Tactic:
add_comm,

Goal state after:
α : Type u
inst✝ : Semiring α
I : Ideal α
a : α
m n : ℕ
ha : a ^ m ∈ I
h : m ≤ n
⊢ a ^ (n - m + m) ∈ I
Module: Mathlib.RingTheory.Ideal.Lattice

Goal state before:
pp: K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ ¬I = ⊤ → I = ⊥

Tactic:
change _ ≠ _ → _

Goal state after:
K : Type u
inst✝ : DivisionSemiring K
I : Ideal K
⊢ I ≠ ⊤ → I = ⊥
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i).1 + (i, n - i).2 = n

Tactic:
add_comm,

Goal state after:
n : ℕ
x✝ : Fin (n + 1)
i : ℕ
h : i < n + 1
⊢ (i, n - i).2 + (i, n - i).1 = n
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
add_comm,

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x + y, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
add_comm,

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y + x} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
sub_add_cancel

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

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

Tactic:
sub_add_cancel

Goal state after:
α : Type u
inst✝ : Ring α
x y : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {y * z + x, y} = span {x, y}

Tactic:
add_comm,

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x + y * z, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, x * z + y} = span {x, y}

Tactic:
add_comm,

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y + x * z} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x - y * z + y * ?z, y} = span {x, y}

pp: case z
α : Type u
inst✝ : CommRing α
x y z : α
⊢ α

Tactic:
sub_add_cancel

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y} = span {x, y}
Module: Mathlib.RingTheory.Ideal.Span

Goal state before:
pp: α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y - x * z + x * ?z} = span {x, y}

pp: case z
α : Type u
inst✝ : CommRing α
x y z : α
⊢ α

Tactic:
sub_add_cancel

Goal state after:
α : Type u
inst✝ : CommRing α
x y z : α
⊢ span {x, y} = span {x, y}
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:
Submodule.quotientRel_def

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.RingTheory.Ideal.Maximal

Goal state before:
pp: case isUnit_or_isUnit.refine_1
α : 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)
⊢ span {a} = span {a * (c * d)}

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:
· apply le_antisymm <;> rw [span_singleton_le_span_singleton]
      · exact (dvd_mul_right (a * (c * d)) a).trans (ha.trans (by ring)).symm.dvd
      · apply dvd_mul_right

Goal state after:
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))
Module: Mathlib.RingTheory.Ideal.Quotient.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : (Submodule.quotientRel I) c₁ c₂
hm : (Submodule.quotientRel (pi fun x ↦ I)) m₁ m₂
⊢ c₁ • m₁ - c₂ • m₂ ∈ pi fun x ↦ I

Tactic:
Submodule.quotientRel_def

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
inst✝¹ : Ring R
I J : Ideal R
a b : R
inst✝ : I.IsTwoSided
c : R ⧸ I
m : (ι → R) ⧸ pi fun x ↦ I
c₁ : R
m₁ : ι → R
c₂ : R
m₂ : ι → R
hc : c₁ - c₂ ∈ I
hm : m₁ - m₂ ∈ pi fun x ↦ I
⊢ c₁ • m₁ - c₂ • m₂ ∈ pi fun x ↦ I
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : (u ∪ s) ∩ (u ∪ t) = u
⊢ u = (u ∪ s) ∩ (u ∪ t)

Tactic:
eq_comm

Goal state after:
α : Type u
ι : Sort x
f : ι → Filter α
s✝ : Set α
hs✝ : s✝ ∈ iInf f
p : Set α → Prop
uni : p univ
ins : ∀ {i : ι} {s₁ s₂ : Set α}, s₁ ∈ f i → p s₂ → p (s₁ ∩ s₂)
p_of_f : ∀ (i : ι), ∀ s ∈ f i, p s
q : Set α → Prop := fun t ↦ t ∈ iInf f ∧ ∀ (t' : Set α), t ⊆ t' → p t'
q_mono : Monotone q
i : ι
s : Set α
hs : s ∈ f i
t : Set α
ht : q t
u : Set α
hu : u = (u ∪ s) ∩ (u ∪ t)
⊢ u = (u ∪ s) ∩ (u ∪ t)
Module: Mathlib.Order.Filter.Map

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α
s : Set β
F : Filter (α × β)
⊢ {y | x = y.1 → y.2 ∈ s} ∈ F ↔ {p | p.1 = x → p.2 ∈ s} ∈ F

Tactic:
eq_comm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
x✝ : xᶜ ∈ f
⊢ sᶜ = m '' x ↔ m '' x = sᶜ

Tactic:
eq_comm

Goal state after:
α : Type u_1
β : Type u_2
m : α → β
f : Filter α
s : Set β
x : Set α
x✝ : xᶜ ∈ f
⊢ m '' x = sᶜ ↔ m '' x = sᶜ
Module: Mathlib.Order.Filter.Basic

Goal state before:
pp: α : Type u
s t : Set α
l : Filter α
⊢ t ∈ l ⊓ 𝓟 s ↔ l ⊓ 𝓟 s ≤ l ⊓ 𝓟 t

Tactic:
by
    simp only [le_inf_iff, inf_le_left, true_and, le_principal_iff]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ t ⊆ m '' s ↔ SurjOn m s t

Tactic:
SurjOn

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ t ⊆ m '' s ↔ t ⊆ m '' s
Module: Mathlib.Order.Filter.AtTopBot.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∃ᶠ (n : ℕ) in atTop, P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
rw [frequently_atTop'] at h
  exact Nat.exists_strictMono_subsequence h

Goal state after: