mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.LinearCombination

Goal state before:
pp: α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Finset α
f : α → R
g : α → M
hf : ∀ (a : α), f a ≠ 0 → a ∈ s
⊢ (linearCombination R g) (onFinset s f hf) = ∑ x ∈ s, f x • g x

Tactic:
by
  classical
  simp only [linearCombination_apply, Finsupp.sum, Finsupp.onFinset_apply, Finsupp.support_onFinset]
  rw [Finset.sum_filter_of_ne]
  intro x _ h
  contrapose h
  simp [h]

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

Goal state before:
pp: M : Type u_7
α : Type u_8
inst✝³ : CommMonoidWithZero M
inst✝² : PartialOrder M
inst✝¹ : ZeroLEOneClass M
inst✝ : PosMulMono M
H : HasFiniteMulSupport fun x ↦ 0
⊢ HasFiniteMulSupport fun x ↦ 1

Tactic:
by fun_prop

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

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding ((Ico (↑a) n).attachFin ⋯) = Ico (↑a) n

Tactic:
map_valEmbedding_attachFin

Goal state after:
n : ℕ
a : Fin n
⊢ Ico (↑a) n = Ico (↑a) n
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding ((Ioo (↑a) n).attachFin ⋯) = Ioo (↑a) n

Tactic:
map_valEmbedding_attachFin

Goal state after:
n : ℕ
a : Fin n
⊢ Ioo (↑a) n = Ioo (↑a) n
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding ((Iic ↑a).attachFin ⋯) = Iic ↑a

Tactic:
map_valEmbedding_attachFin

Goal state after:
n : ℕ
a : Fin n
⊢ Iic ↑a = Iic ↑a
Module: Mathlib.Order.Interval.Finset.Fin

Goal state before:
pp: n : ℕ
a : Fin n
⊢ map valEmbedding ((Iio ↑a).attachFin ⋯) = Iio ↑a

Tactic:
map_valEmbedding_attachFin

Goal state after:
n : ℕ
a : Fin n
⊢ Iio ↑a = Iio ↑a
Module: Mathlib.Data.Fin.VecNotation

Goal state before:
pp: α : Type u
x y : α
u : Fin 0 → α
⊢ Set.range (vecCons x (vecCons y u)) = {x, y}

Tactic:
rw [range_cons, range_cons_empty, Set.singleton_union]

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

Goal state before:
pp: ι : Type u_1
R : Type u_3
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
⊢ (↑b.repr).range = supported R R univ

Tactic:
rw [LinearEquiv.range, Finsupp.supported_univ]

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

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ 0 ^ ↑y = 0

Tactic:
epow_natCast,

Goal state after:
case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ 0 ^ y = 0
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
⊢ 1 ^ ↑y = 1

Tactic:
epow_natCast,

Goal state after:
case coe
y✝ : ℕ∞
y : ℕ
⊢ 1 ^ y = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ ⊤ ^ ↑y = ⊤

Tactic:
epow_natCast,

Goal state after:
case coe
y✝ : ℕ∞
y : ℕ
h : ↑y ≠ 0
⊢ ⊤ ^ y = ⊤
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
⊢ x ^ ↑0 = 1

Tactic:
epow_natCast,

Goal state after:
x : ℕ∞
⊢ x ^ 0 = 1
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: x : ℕ∞
⊢ x ^ ↑1 = x

Tactic:
epow_natCast,

Goal state after:
x : ℕ∞
⊢ x ^ 1 = x
Module: Mathlib.Data.ENat.Pow

Goal state before:
pp: case top.inl
x y z : ℕ∞
x_0 : x < 1
⊢ (x * y) ^ ⊤ = x ^ ⊤ * y ^ ⊤

Tactic:
simp only [Order.lt_one_iff.1 x_0, zero_mul, zero_epow_top]

Goal state after:
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
p a b c : G
⊢ c + a ≡ b [PMOD p] ↔ a + c ≡ b [PMOD p]

Tactic:
by rw [add_comm]

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

Goal state before:
pp: M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≤ i, f i.succ j = (∏ i, ∏ j ≥ i, f i.castSucc j) * ∏ i, ∏ j ≥ i, f j.succ i

Tactic:
congr 1

Goal state after:
case e_a
M : Type u_2
inst✝ : CommMonoid M
n : ℕ
f : Fin (n + 1) → Fin n → M
⊢ ∏ i, ∏ j ≤ i, f i.succ j = ∏ i, ∏ j ≥ i, f j.succ i
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (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
w : ι → G
s : Finset ι
⊢ ∀ (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i

Tactic:
g₁

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_6
hG : Group G
inst✝³ : MulAction G R
inst✝² : SMul G M
inst✝¹ : IsScalarTower G R M
inst✝ : SMulCommClass G R M
v : ι → M
hv :
  ∀ (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
w : ι → G
s : Finset ι
g₁ : ι → R
⊢ ∀ (g : ι → R), (∀ i ∉ s, g₁ i = g i) → ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), g₁ i = g i
Module: Mathlib.Algebra.Group.ModEq

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℕ
left✝ : k < n
j : ℤ
hj : a - b = (j * ↑n + ↑k) • p
⊢ ∃ m, a - b = m • p

Tactic:
rw [hj]

Goal state after:
case mpr
G : Type u_1
inst✝ : AddCommGroup G
p a b : G
n : ℕ
hn : n ≠ 0
k : ℕ
left✝ : k < n
j : ℤ
hj : a - b = (j * ↑n + ↑k) • p
⊢ ∃ m, (j * ↑n + ↑k) • p = m • p
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (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
w : ι → Rˣ
s : Finset ι
⊢ ∀ (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), f i = g i

Tactic:
g₁

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
hv :
  ∀ (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
w : ι → Rˣ
s : Finset ι
g₁ : ι → R
⊢ ∀ (g : ι → R), (∀ i ∉ s, g₁ i = g i) → ∑ i ∈ s, g₁ i • (w • v) i = ∑ i ∈ s, g i • (w • v) i → ∀ (i : ι), g₁ i = g i
Module: Mathlib.Data.Nat.GCD.Basic

Goal state before:
pp: a b c : ℕ
⊢ (a ^ b - 1).gcd (a ^ c - 1) = a ^ b.gcd c - 1

Tactic:
by
  rcases eq_zero_or_pos b with rfl | hb
  · simp
  replace hb : c % b < b := mod_lt c hb
  rw [gcd_rec, pow_sub_one_mod_pow_sub_one, pow_sub_one_gcd_pow_sub_one, ← gcd_rec]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
⊢ LinearIndependent R (w • v) ↔ LinearIndependent R v

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h.units_smul w⟩

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
v : ι → M
w : ι → Rˣ
h : LinearIndependent R (w • v)
⊢ LinearIndependent R v
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: case neg
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 + 0 = a % c + b % c

Tactic:
add_zero

Goal state after:
case neg
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 = a % c + b % c
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = (a + b) % c + 0

Tactic:
add_zero

Goal state after:
a b c : ℕ
hc : a % c + b % c < c
⊢ (a + b) % c = (a + b) % c
Module: Mathlib.Data.Nat.ModEq

Goal state before:
pp: a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ a / c + b / c + 0 = a / c + b / c

Tactic:
add_zero

Goal state after:
a b c : ℕ
hc : a % c + b % c < c
hc0 : ¬c = 0
⊢ a / c + b / c = a / c + b / c
Module: Mathlib.LinearAlgebra.LinearIndependent.Basic

Goal state before:
pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (g a • ⇑a + 0) 1

pp: G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ ∀ x ∈ s, g x • ⇑x = 0

Tactic:
add_zero

Goal state after:
G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ (g a • ⇑a) 1 = (g a • ⇑a) 1

G : Type u_6
inst✝² : MulOneClass G
L : Type u_7
inst✝¹ : CommRing L
inst✝ : IsDomain L
this✝ : DecidableEq (G →* L) := Classical.decEq (G →* L)
this : MulAction L L := Semiring.toModule.toMulAction
a : G →* L
s : Finset (G →* L)
has : a ∉ s
ih : ∀ (g : (G →* L) → L), ∑ i ∈ s, g i • ⇑i = 0 → ∀ i ∈ s, g i = 0
g : (G →* L) → L
hg : ∑ i ∈ insert a s, g i • ⇑i = 0
h1 : ∀ i ∈ s, g i • ⇑i = g i • ⇑a
h2 : ∀ i ∈ s, ∃ y, i y ≠ a y
h3 : ∀ i ∈ s, g i = 0
⊢ ∀ x ∈ s, g x • ⇑x = 0
Module: Mathlib.LinearAlgebra.Dimension.Basic

Goal state before:
pp: case a
R : Type u
M : Type v
M' : Type v'
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
s : Set ↥f.range
li : LinearIndepOn R id s
⊢ lift.{v, v'} #↑↑⟨s, li⟩ ≤ lift.{v', v} #↑↑⟨rangeSplitting ⇑f '' s, ⋯⟩

Tactic:
exact (Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
⊢ Module.rank R ↥s ≤ Module.rank R M

Tactic:
rw [← rank_top R M]
  exact rank_mono le_top

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

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
p : α → Prop
x : α
hx : ¬p x
this : Fintype α
⊢ Nat.card { x // p x } < Nat.card α

Tactic:
simpa only [Nat.card_eq_fintype_card, gt_iff_lt] using Fintype.card_subtype_lt hx

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ a₁ ∈ s, ∀ a₂ ∈ s, a₁ ≠ a₂ → f a₁ ≠ f a₂
⊢ s.encard ≤ t.encard

Tactic:
suffices Function.Injective (hf.restrict f) by
    let f' : s ↪ t := ⟨hf.restrict, this⟩
    exact f'.encard_le

Goal state after:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hf : MapsTo f s t
hc : ∀ a₁ ∈ s, ∀ a₂ ∈ s, a₁ ≠ a₂ → f a₁ ≠ f a₂
⊢ Function.Injective (MapsTo.restrict f s t hf)
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
⊢ (insert a s).ncard = s.ncard

Tactic:
by
  rw [insert_eq_of_mem h]

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

Goal state before:
pp: α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ ↑(s \ {a}).ncard + 1 = s.encard

Tactic:
hs.sdiff.cast_ncard_eq,

Goal state after:
α : Type u_1
s : Set α
a : α
h : a ∈ s
hs : s.Finite
⊢ (s \ {a}).encard + 1 = s.encard
Module: Mathlib.Data.Set.Card

Goal state before:
pp: α : Type u_1
s : Set α
a : α
⊢ (s \ {a}).ncard ≤ s.ncard

Tactic:
by
  obtain hs | hs := s.finite_or_infinite
  · apply ncard_le_ncard sdiff_subset hs
  convert! Nat.zero_le _
  exact (hs.sdiff (by simp)).ncard

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : α → β
y : β
hs : s.Finite
⊢ {x | x ∈ s ∧ f x = y}.ncard ≠ 0 ↔ y ∈ f '' s

Tactic:
refine ⟨nonempty_of_ncard_ne_zero, ?_⟩
  rintro ⟨z, hz, rfl⟩
  exact @ncard_ne_zero_of_mem _ ({ x ∈ s | f x = f z }) z (mem_sep hz rfl)
    (hs.subset (sep_subset _ _))

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

Goal state before:
pp: α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ (t \ s).ncard = (t \ s).ncard + s.ncard - s.ncard

Tactic:
add_tsub_cancel_right

Goal state after:
α : Type u_1
s t : Set α
hst : s ⊆ t
ht : t.Finite
⊢ (t \ s).ncard = (t \ s).ncard
Module: Mathlib.Algebra.Group.Fin.Tuple

Goal state before:
pp: α : Type u_1
inst✝ : Zero α
⊢ ![] = 0

Tactic:
Matrix.zero_empty

Goal state after:
α : Type u_1
inst✝ : Zero α
⊢ ![] = ![]
Module: Mathlib.Data.Set.Card

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

Tactic:
by
  rw [← compl_empty_iff, ← ncard_eq_zero, ← ncard_add_ncard_compl s, left_eq_add]

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

Goal state before:
pp: case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ (Set.range g)ᶜ.ncard ≤ 1

Tactic:
Set.ncard_le_one

Goal state after:
case inr.refine_2
α : Type u_1
β : Type u_2
inst✝ : Finite α
f : α → β
hf✝ : Surjective f
h✝ : Nonempty α
g : β → α := surjInv hf✝
hf : ∀ (b : β), f (g b) = b
h : ∀ (a b c d : α), f a = f b → f c = f d → a ≠ b → c ≠ d → {a, b} = {c, d}
⊢ ∀ a ∈ (Set.range g)ᶜ, ∀ b ∈ (Set.range g)ᶜ, a = b
Module: Mathlib.RingTheory.Congruence.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
H : ∀ (x y : R), c x y ↔ d x y
⊢ ⇑c = ⇑d

Tactic:
by ext; apply H

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

Goal state before:
pp: R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ (ringConGen r).comap f = ringConGen (r on ⇑f)

Tactic:
refine le_antisymm ?_ (le_comap_ringConGen _ _)

Goal state after:
R : Type u_5
R' : Type u_6
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring R'
r : R' → R' → Prop
f : R ≃+* R'
⊢ (ringConGen r).comap f ≤ ringConGen (r on ⇑f)
Module: Mathlib.LinearAlgebra.Pi

Goal state before:
pp: R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ∀ ⦃x : (i : ι) → φ i⦄, ((∀ i ∈ Iᶜ, x i = 0) ∧ ∀ i ∈ Jᶜ, x i = 0) → ∀ (x_1 : ι), x x_1 = 0 x_1

Tactic:
rintro b ⟨hI, hJ⟩ i

Goal state after:
R : Type u
ι : Type x
inst✝³ : Semiring R
φ : ι → Type i
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ i ∈ Iᶜ, b i = 0
hJ : ∀ i ∈ Jᶜ, b i = 0
i : ι
⊢ b i = 0 i
Module: Mathlib.LinearAlgebra.Prod

Goal state before:
pp: R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
⊢ (f.coprod g).ker ≤ f.ker.prod g.ker

Tactic:
rintro ⟨y, z⟩ h

Goal state after:
R : Type u
M : Type v
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M₂ : Type u_3
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
M₃ : Type u_4
inst✝¹ : AddCommGroup M₃
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
hd : Disjoint f.range g.range
y : M
z : M₂
h : (y, z) ∈ (f.coprod g).ker
⊢ (y, z) ∈ f.ker.prod g.ker
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₂
⊢ p₁.prod p₂ = ⊤ ↔ p₁ = ⊤ ∧ p₂ = ⊤

Tactic:
by
  simp only [eq_top_iff, le_prod_iff, map_top, range_fst, range_snd]

Goal state after:
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
⊢ IsGLB (Set.Ioc i j) i

Tactic:
have h := succFn_spec i

Goal state after:
ι : 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 : IsGLB (Set.Ioi i) (succFn i)
⊢ IsGLB (Set.Ioc i j) i
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
⊢ succFn i ≤ j

Tactic:
have h := succFn_spec i

Goal state after:
ι : Type u_1
inst✝ : LinearOrder ι
i j : ι
hij : i < j
h : IsGLB (Set.Ioi i) (succFn i)
⊢ succFn i ≤ j
Module: Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁶ : CommMonoid M
inst✝⁵ : LinearOrder α
inst✝⁴ : LocallyFiniteOrderBot α
inst✝³ : Add α
inst✝² : One α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
a : α
f : α → M
⊢ ∏ i < a + 1, f i = (∏ i < a, f i) * f a

Tactic:
simp_rw [prod_Iio_add_one_comm, mul_comm]

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

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ (∏ x, ∏ x_1 > x, f x_1 x) * ∏ x, ∏ x_1 > x, f x x_1 = (∏ x, ∏ x_1 > x, f x_1 x) * ∏ x, ∏ x_1 < x, f x_1 x

Tactic:
congr 1

Goal state after:
case e_a
α : Type u_1
M : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : LinearOrder α
inst✝² : Fintype α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : LocallyFiniteOrderBot α
f : α → α → M
⊢ ∏ x, ∏ x_1 > x, f x x_1 = ∏ x, ∏ x_1 < x, f x_1 x
Module: Mathlib.Algebra.BigOperators.Intervals

Goal state before:
pp: case pos
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

pp: case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n < m
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
· rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]

Goal state after:
case neg
M : Type u_3
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n < m
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ toZ hι.some (succ^[n.toNat] hι.some) = n

Tactic:
toZ_iterate_succ

Goal state after:
case inl
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : NoMinOrder ι
hι : Nonempty ι
n : ℤ
hn : 0 ≤ n
⊢ ↑n.toNat = n
Module: Mathlib.Order.SuccPred.LinearLocallyFinite

Goal state before:
pp: ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (toZ ⊥ (succ^[n] ⊥)).toNat = n

Tactic:
toZ_iterate_succ

Goal state after:
ι : Type u_1
inst✝⁵ : LinearOrder ι
inst✝⁴ : SuccOrder ι
inst✝³ : PredOrder ι
inst✝² : IsSuccArchimedean ι
inst✝¹ : NoMaxOrder ι
inst✝ : OrderBot ι
n : ℕ
⊢ (↑n).toNat = n
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
⊢ i + k - k = i

Tactic:
add_tsub_cancel_right

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

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ a.1 ≤ k) = (fun a ↦ a.2 ≤ k) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = k ∧ a = i ∧ b + (n - k) = j ↔ a + b = k ∧ a = i ∧ b + (n - k) = j

Tactic:
by rw [add_comm]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ p ∈ antidiagonal n, f p.swap = ∏ p ∈ antidiagonal n, f p

Tactic:
conv_lhs => rw [← map_swap_antidiagonal, Finset.prod_map]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
n : ℕ
f : ℕ × ℕ → M
⊢ ∏ x ∈ antidiagonal n, f ({ toFun := Prod.swap, inj' := ⋯ } x).swap = ∏ p ∈ antidiagonal n, f p
Module: Mathlib.Data.Finset.NatAntidiagonal

Goal state before:
pp: n k : ℕ
h : k ≤ n
aux₁ : (fun a ↦ k ≤ a.2) = (fun a ↦ k ≤ a.1) ∘ ⇑(Equiv.prodComm ℕ ℕ).symm
i j a b : ℕ
⊢ b + a = n - k ∧ a = i ∧ b + k = j ↔ a + b = n - k ∧ a = i ∧ b + k = j

Tactic:
by rw [add_comm]

Goal state after:
Module: Mathlib.Algebra.Ring.Idempotent

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

Tactic:
by
  rw [mul_sub, mul_one, h.eq, sub_self]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) + x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) =
    x * (x ^ i * y ^ (n - i) * ↑(n.choose i)) + y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))

Tactic:
congr 1

Goal state after:
case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i) = x * (x ^ i * y ^ (n - i) * ↑(n.choose i))

case e_a
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = y * (x ^ i.succ * y ^ (n - i.succ) * ↑(n.choose i.succ))
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| a * a + 0

Tactic:
add_zero

Goal state after:
R : Type u_1
inst✝ : Semiring R
a b : R
mul : a * b = 0
add : a + b = 1
| a * a
Module: Mathlib.Algebra.Ring.Idempotent

Goal state before:
pp: R : Type u_1
a b : R
inst✝¹ : NonUnitalSemiring R
inst✝ : IsAddTorsionFree R
ha : IsIdempotentElem a
hab : a * b + b * a = 0
⊢ a * b = 0

Tactic:
by
  have h : a * b * a = 0 := by
    rw [← nsmul_right_inj ((Nat.zero_ne_add_one 1).symm), nsmul_zero]
    have : a * (a * b + b * a) * a = 0 := by rw [hab, mul_zero, zero_mul]
    simp_rw [mul_add, add_mul, mul_assoc, ha.eq, ← mul_assoc, ha.eq, ← two_nsmul] at this
    exact this
  suffices a * a * b + a * b * a = 0 by rwa [h, add_zero, ha.eq] at this
  rw [mul_assoc, mul_assoc, ← mul_add, hab, mul_zero]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
n✝ : ℕ
t : ℕ → ℕ → R := fun n m ↦ x ^ m * y ^ (n - m) * ↑(n.choose m)
h_first : ∀ (n : ℕ), t n 0 = y ^ n
h_last : ∀ (n : ℕ), t n n.succ = 0
n i : ℕ
h_mem : i ∈ range n.succ
h_le : i ≤ n
h_eq : ¬i = n
⊢ x ^ i.succ * y ^ (n.succ - i.succ) * ↑(n.choose i.succ) = x ^ i.succ * y * y ^ (n - i.succ) * ↑(n.choose i.succ)

Tactic:
· rw [succ_sub (lt_of_le_of_ne h_le h_eq)]
        rw [pow_succ' y, mul_assoc, mul_assoc, mul_assoc, mul_assoc]

Goal state after: