mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case mk.mk.e_a.refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
a✝ : i ∈ (sf + sg).toFinset
⊢ i ∉ sg.toFinset → (φ i) (g i) = 0

Tactic:
H2

Goal state after:
case mk.mk.e_a.refine_2
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → β i →+ γ
f : (i : ι) → β i
support'✝¹ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
g : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ g i = 0 }
sg : Multiset ι
hg : ∀ (i : ι), i ∈ sg ∨ g i = 0
i : ι
a✝ : i ∈ (sf + sg).toFinset
H2 : i ∉ sg.toFinset
⊢ (φ i) (g i) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
⊢ x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f) ↔ ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)

Tactic:
refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
x✝ : x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f)
i : ι
hi : i ∈ Set.univ
y : Π₀ (i : ι), β₁ i
hy : (mapRange.addMonoidHom f) y = x
⊢ x i ∈ (fun i ↦ ((fun i ↦ AddMonoidHom.mrange (f i)) i).carrier) i

case refine_2
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
⊢ x ∈ AddMonoidHom.mrange (mapRange.addMonoidHom f)
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case neg
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∉ x.support
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = x i

Tactic:
DFinsupp.notMem_support_iff.mp mem,

Goal state after:
case neg
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst✝¹ : (i : ι) → AddCommMonoid (β₁ i)
inst✝ : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → β₁ i →+ β₂ i
x : Π₀ (i : ι), β₂ i
h : ⇑x ∈ AddSubmonoid.pi Set.univ fun i ↦ AddMonoidHom.mrange (f i)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i) (g i) = x i
i : ι
mem : i ∉ x.support
⊢ (f i) ((mk x.support fun x_1 ↦ g ↑x_1) i) = 0
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i ≠ 0
⊢ ((fun i ↦ (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ i, ⨆ (_ : p i), S i

Tactic:
refine mem_iSup_of_mem i ?_

Goal state after:
case a
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
S : ι → Submodule R N
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i ≠ 0
⊢ ((fun i ↦ (S i).subtype) i).toAddMonoidHom (((filterLinearMap R (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
⊢ LinearIndependent R ![-x, y] ↔ LinearIndependent R ![x, y]

Tactic:
by
  rw [pair_iff, pair_iff]
  refine ⟨fun h s t hst ↦ ?_, fun h s t hst ↦ ?_⟩ <;> simpa using h (-s) t (by simpa using hst)

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

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
u : S
hu : u ≠ 0
h : ∀ (s t : R), s • u • x + t • u • y = 0 → s = 0 ∧ t = 0
s t : R
hst : s • x + t • y = 0
⊢ s • u • x + t • u • y = 0

Tactic:
by rw [← smul_comm u s, ← smul_comm u t, ← smul_add, hst, smul_zero]

Goal state after:
Module: Mathlib.Tactic.Module

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ r • l.eval = (r • l).eval

Tactic:
eval_smul

Goal state after:
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ r • l.eval = r • ?m.57

case h
S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ ?m.57 = l.eval

S : Type u_1
R : Type u_2
M : Type u_3
R₀ : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₀
inst✝² : Module R₀ M
inst✝¹ : Semiring S
inst✝ : Module S M
l : NF R M
l₀ : NF R₀ M
s : S
r : R
x : M
hx : x = l₀.eval
hl : l.eval = l₀.eval
hs : r • x = s • x
⊢ M
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R v

Tactic:
rw [linearIndependent_iff]

Goal state after:
R : Type u_3
N : Type u_6
inst✝⁴ : Ring R
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
⊢ ∀ (l : ι →₀ R), (Finsupp.linearCombination R v) l = 0 → l = 0
Module: Mathlib.Algebra.Algebra.Opposite

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Semiring A
inst✝⁶ : Semiring B
inst✝⁵ : Algebra R S
inst✝⁴ : Algebra R A
inst✝³ : Algebra R B
inst✝² : Algebra S A
inst✝¹ : SMulCommClass R S A
inst✝ : IsScalarTower R S A
c : R
x : Aᵐᵒᵖ
⊢ unop (c • x) = unop (((algebraMap R A).toOpposite ⋯) c * x)

Tactic:
by
    simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul,
      Algebra.smul_def, Algebra.commutes, unop_op]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • (linearCombination R f) l' - r • l' i • f i + l' i • r • m = 0
⊢ l' = 0

Tactic:
hg,

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝³ : DecidableEq ι
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
hf : ∀ (l : ι →₀ R), (linearCombination R f) l = 0 → l = 0
i : ι
m : M
r : R
hr : r ∈ nonZeroDivisors R
l : ι →₀ R
hl : l i ∈ nonZeroDivisors R
hg : r • m = (linearCombination R f) l
l' : ι →₀ R
hl' : r • (linearCombination R f) l' - r • l' i • f i + l' i • (linearCombination R f) l = 0
⊢ l' = 0
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M₀ : Type u_2
inst✝² : AddGroup A
inst✝¹ : MonoidWithZero M₀
inst✝ : Nontrivial M₀
ψ : AddChar A M₀
h : ψ 0 = 0 0
⊢ False

Tactic:
by simpa only [h, Pi.zero_apply, zero_ne_one] using map_zero_eq_one ψ

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
s' : Submonoid (Multiplicative M) := Submonoid.closure s
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' s)

Tactic:
have h' : Submonoid.map (of R M) s' = Submonoid.closure (of R M '' s) :=
    MonoidHom.map_mclosure _ _

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddMonoid M
inst✝ : Nontrivial R
m : M
s : Set M
h : of' R M m ∈ Submodule.span R ↑(Submonoid.closure (of' R M '' s))
s' : Submonoid (Multiplicative M) := Submonoid.closure s
h' : Submonoid.map (of R M) s' = Submonoid.closure (⇑(of R M) '' s)
⊢ Multiplicative.ofAdd m ∈ Submonoid.closure (⇑Multiplicative.toAdd ⁻¹' s)
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #s * #t ↔ InjOn (fun x ↦ f x.1 x.2) (↑s ×ˢ ↑t)

Tactic:
← card_product,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
⊢ #(image₂ f s t) = #(s ×ˢ t) ↔ InjOn (fun x ↦ f x.1 x.2) (↑s ×ˢ ↑t)
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g' s) t)

Tactic:
by
    push_cast
    exact image_image2_distrib_left h_distrib

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
h : ∃ x, ∃ (_ : x ∈ s), ¬Disjoint (image (f a) t) (image (f x) t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)

Tactic:
obtain ⟨b, hb, h⟩ := h

Goal state after:
case neg
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s✝ : Finset α
t : Finset β
a : α
s : Finset α
a✝ : a ∉ s
ih : #t ∣ #(image₂ f s t)
hf : ∀ a_1 ∈ insert a s, Injective (f a_1)
hs : ((fun a ↦ image (f a) t) '' ↑(insert a s)).PairwiseDisjoint id
b : α
hb : b ∈ s
h : ¬Disjoint (image (f a) t) (image (f b) t)
⊢ #t ∣ #(image (fun b ↦ f a b) t ∪ image₂ f s t)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x y : R[M]
a✝ : Multiplicative M
⊢ (MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) (x * y).coeff)).coeff a✝ =
    (MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff) *
          MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) y.coeff)).coeff
      a✝

Tactic:
simp [MonoidAlgebra.coeff_mul, coeff_mul, sum_mapDomain_index, add_mul, mul_add, ite_add_zero,
      Multiplicative.ext_iff]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Opposite

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
⊢ MonoidAlgebra.opRingEquiv.symm (single x r) = op (single (unop x) (unop r))

Tactic:
apply MulOpposite.unop_injective

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
⊢ unop (MonoidAlgebra.opRingEquiv.symm (single x r)) = unop (op (single (unop x) (unop r)))
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔
    ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b

Tactic:
refine ⟨fun h p1 p2 ⟨⟨ha1, hb1⟩, he1⟩ ⟨⟨ha2, hb2⟩, he2⟩ ↦ ?_, fun h a b ha hb he ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : UniqueMul A B a0 b0
p1 p2 : G × G
x✝¹ : (p1.1 ∈ A ∧ p1.2 ∈ B) ∧ p1.1 * p1.2 = a0 * b0
x✝ : (p2.1 ∈ A ∧ p2.2 ∈ B) ∧ p2.1 * p2.2 = a0 * b0
ha1 : p1.1 ∈ A
hb1 : p1.2 ∈ B
he1 : p1.1 * p1.2 = a0 * b0
ha2 : p2.1 ∈ A
hb2 : p2.2 ∈ B
he2 : p2.1 * p2.2 = a0 * b0
⊢ p1 = p2

case refine_2
G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
h : ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = a0 * b0
⊢ a = a0 ∧ b = b0
Module: Mathlib.Order.Sublattice

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
a : α
S : Set (Sublattice α)
⊢ a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L

Tactic:
by
  rw [← SetLike.mem_coe]; simp

Goal state after:
Module: Mathlib.Order.Sublattice

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : Lattice α
a : α
f : ι → Sublattice α
⊢ a ∈ ⨅ i, f i ↔ ∀ (i : ι), a ∈ f i

Tactic:
by
  rw [← SetLike.mem_coe]; simp

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
⊢ IsSMulRegular R[X] s

Tactic:
rintro ⟨f⟩ ⟨g⟩ hfg

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : (fun x ↦ s • x) { toFinsupp := f } = (fun x ↦ s • x) { toFinsupp := g }
⊢ { toFinsupp := f } = { toFinsupp := g }
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ p = 0

Tactic:
rw [← one_smul R p, ← h, zero_smul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
i j : ℕ
⊢ (monomial i) a = (monomial j) a ↔ i = j

Tactic:
by
  simp [monomial_eq_monomial_iff, ha]

Goal state after:
Module: Mathlib.LinearAlgebra.StdBasis

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
h1 : φ 1 = 1
⊢ ∃ s, φ = Pi.evalAlgHom k (fun i ↦ k) s

Tactic:
have := Fintype.ofFinite G

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : NoZeroDivisors k
inst✝¹ : Nontrivial k
inst✝ : Finite G
φ : (G → k) →ₐ[k] k
h1 : φ 1 = 1
this : Fintype G
⊢ ∃ s, φ = Pi.evalAlgHom k (fun i ↦ k) s
Module: Mathlib.RingTheory.Finiteness.Finsupp

Goal state before:
pp: case a.refine_2.right
R : Type u_1
M : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
s : Submodule R M
this✝¹ : DecidableEq R
this✝ : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R ↑t1 = map f s
t2 : Finset M
ht2 : span R ↑t2 = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ f (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : l ∈ supported R R ↑t1
hl2 : (linearCombination R id) l = f x
⊢ x - (linearCombination R id) ((lmapDomain R R g) l) ∈ f.ker

Tactic:
· rw [LinearMap.mem_ker, f.map_sub, ← hl2]
    rw [Finsupp.linearCombination_apply, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply]
    rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]
    · rw [sub_eq_zero]
      refine Finset.sum_congr rfl fun y hy => ?_
      unfold id
      rw [f.map_smul, (hg y (hl1 hy)).2]
    · exact zero_smul _
    · exact fun _ _ _ => add_smul _ _ _

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inl
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc, (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ) ∈ r

Tactic:
convert! p.step ⟨i.1, hi⟩

Goal state after:
case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc = p.toFun ⟨↑i, hi⟩.castSucc

case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : i < Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)
⊢ (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ = p.toFun ⟨↑i, hi⟩.succ
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_1
G : Type u
H : Type v
inst✝³ : Mul G
inst✝² : Mul H
inst✝¹ : TwoUniqueProds G
inst✝ : TwoUniqueProds H
this : ∀ (b : Bool), TwoUniqueProds (I G H b)
⊢ TwoUniqueProds (G × H)

Tactic:
refine of_injective_mulHom (Prod.upMulHom G H) (fun x y he ↦ Prod.ext ?_ ?_)
      (TwoUniqueProds.instForall <| I G H) <;> apply up_injective
    exacts [congr_fun he false, congr_fun he true]

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + 1)
⊢ (p.append q connect).toFun (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) = p.toFun i

Tactic:
delta append

Goal state after:
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + 1)
⊢ { length := p.length + q.length + 1, toFun := Fin.append p.toFun q.toFun ∘ Fin.cast ⋯, step := ⋯ }.toFun
      (Fin.cast ⋯ (Fin.castAdd (q.length + 1) i)) =
    p.toFun i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case hl
α : Type u_1
r : SetRel α α
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ (p.append q connect).toList.length = (p.toList ++ q.toList).length

Tactic:
simp; grind

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 = ↑m
⊢ (x, y) ∈ r

Tactic:
· convert! connect_next
        · change Fin.insertNth _ _ _ _ = _
          rw [show m.castSucc = i.succ.castSucc from Fin.ext hm.symm, Fin.insertNth_apply_same]
        · change Fin.insertNth _ _ _ _ = _
          rw [Fin.insertNth_apply_above]
          swap
          · change i.1 + 1 < m.1 + 1; lia
          simp only [Fin.pred_succ, eq_rec_constant]
          congr; ext; exact hm.symm

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h.right
α : Type u_1
inst✝ : Preorder α
x : α
n : ℕ
hfin : height x < ⊤
m : ℕ
hx : height x = ↑m
h : n < m
p : LTSeries α
hp : RelSeries.last p = x
hlen : p.length = m
⊢ height (p.toFun ⟨n, ⋯⟩) = ↑n

Tactic:
· exact height_eq_index_of_length_eq_height_last (by simp [hlen, hp, hx]) ⟨n, by lia⟩

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
P₂ : Type u_17
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid P₂
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R₂ P₂
inst✝ : Module R P
g h : M ⊗[R] N ⊗[R] P →ₛₗ[σ₁₂] P₂
H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] y ⊗ₜ[R] z) = h (x ⊗ₜ[R] y ⊗ₜ[R] z)
x : M
y : N
z : P
⊢ ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ g)) x) y) z =
    ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ h)) x) y) z

Tactic:
exact H x y z

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring R₂
σ₁₂ : R →+* R₂
M : Type u_7
N : Type u_8
P : Type u_9
P₂ : Type u_17
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid P₂
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R₂ P₂
inst✝ : Module R P
g h : M ⊗[R] (N ⊗[R] P) →ₛₗ[σ₁₂] P₂
H : ∀ (x : M) (y : N) (z : P), g (x ⊗ₜ[R] (y ⊗ₜ[R] z)) = h (x ⊗ₜ[R] (y ⊗ₜ[R] z))
x : M
y : N
z : P
⊢ (((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ g) x)) y) z =
    (((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ h) x)) y) z

Tactic:
exact H x y z

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p.length ≤ height x

Tactic:
suffices p'.length ≤ height p'.last by
      rw [hlast'] at this
      simpa [p'] using this

Goal state after:
case a
α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
⊢ ↑p'.length ≤ height (RelSeries.last p')
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹¹ : IdemSemiring α
inst✝¹⁰ : LE β
inst✝⁹ : LT β
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Max β
inst✝ : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f (a + b) = f a ⊔ f b

Tactic:
add,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
π : ι → Type u_4
inst✝¹¹ : IdemSemiring α
inst✝¹⁰ : LE β
inst✝⁹ : LT β
inst✝⁸ : Zero β
inst✝⁷ : One β
inst✝⁶ : Add β
inst✝⁵ : Mul β
inst✝⁴ : Pow β ℕ
inst✝³ : SMul ℕ β
inst✝² : NatCast β
inst✝¹ : Max β
inst✝ : Bot β
f : β → α
hf : Injective f
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : β}, f x < f y ↔ x < y
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : β), f (x + y) = f x + f y
mul : ∀ (x y : β), f (x * y) = f x * f y
nsmul : ∀ (n : ℕ) (x : β), f (n • x) = n • f x
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
natCast : ∀ (n : ℕ), f ↑n = ↑n
sup : ∀ (a b : β), f (a ⊔ b) = f a ⊔ f b
bot : f ⊥ = ⊥
a b : β
⊢ f a + f b = f a ⊔ f b