mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case pos
R : Type u
inst✝ : EuclideanDomain R
x y : R
h : 0 ∣ y
⊢ 0 = x * (y / 0)

Tactic:
div_zero,

Goal state after:
case pos
R : Type u
inst✝ : EuclideanDomain R
x y : R
h : 0 ∣ y
⊢ 0 = x * 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun i a ↦ (c * a) • f i) = a.sum fun a b ↦ c • b • f a

Tactic:
simp only [zero_smul, mul_smul]

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

Goal state before:
pp: case mp.refine_4
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
I : Ideal R
inst✝ : I.IsTwoSided
ι : Type u_4
f : ι → M
x : M
hx : x ∈ I • span R (Set.range f)
c : R
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
i✝ : ι
⊢ 0 • f i✝ = 0

Tactic:
simp only [zero_smul, mul_smul]

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

Goal state before:
pp: case h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ y * (z * gcdB x y)

Tactic:
mul_comm

Goal state after:
case h₂
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ y * x ∣ y * (z * gcdB x y)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : annihilator R M = ⊤
m m' : M
⊢ m = m'

Tactic:
rw [← one_smul R m, ← one_smul R m']
      simp_rw [mem_annihilator.mp (h ▸ Submodule.mem_top)]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n : ℕ
⊢ ⊤.IsTwoSided

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K L : Ideal R
inst✝ : I.IsTwoSided
m n x✝¹ : ℕ
x✝ : (I ^ x✝¹).IsTwoSided
⊢ IsTwoSided (I ^ x✝¹ * I)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ (N ⊔ P).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
rw [← sSup_pair, sSup_eq_iSup, iSup_subtype', annihilator_iSup, ← iInf_pair, iInf_subtype']

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a

Tactic:
apply Iff.trans Multiset.lcm_dvd

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∀ b ∈ Multiset.map f s.val, b ∣ a) ↔ ∀ b ∈ s, f b ∣ a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommSemiring R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0

Tactic:
rw [Multiset.inf_zero]
    exact le_top

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ f x * a) = s.gcd f * normalize a

Tactic:
mul_comm

Goal state after:
β : Type u_3
α : Type u_5
inst✝¹ : CommMonoidWithZero α
inst✝ : StrongNormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ f x * a) (s.gcd f * a)

Tactic:
mul_comm

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ a * f x) (a * s.gcd f)
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ Associated (s.gcd fun x ↦ a * f x) (a * s.gcd f)

Tactic:
apply gcd_mul_left'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ k ∣ m * gcd k n

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ n * m
⊢ k ∣ gcd k n * m
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : ¬gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k

Tactic:
· rw [gcd_eq_zero_iff] at hg
    rcases hg with ⟨rfl, rfl⟩
    exact
      (gcd_zero_left' (0 ^ k : α)).dvd.trans
        (pow_dvd_pow_of_dvd (gcd_zero_left' (0 : α)).symm.dvd _)

Goal state after:
case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
k : ℕ
hg : ¬gcd a b = 0
⊢ gcd a (b ^ k) ∣ gcd a b ^ k
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ a * b
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Tactic:
mul_comm

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
h1 : IsUnit (gcd (d₁ ^ k) b)
h2 : d₁ ^ k ∣ b * a
⊢ d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₁ * d₂
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
⊢ Associated (d₁ ^ k) a

Tactic:
mul_comm

Goal state after:
case h
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c : α
hab : IsUnit (gcd a b)
k : ℕ
h : b * a = c ^ k
h✝ : Nontrivial α
ha : ¬a = 0
hb : ¬b = 0
hk : k > 0
hc✝ : c ∣ a * b
d₁ d₂ : α
hd₁ : d₁ ∣ a
hd₂ : d₂ ∣ b
hc : c = d₂ * d₁
h0₁ : d₁ ^ k ≠ 0
a' : α
ha' : a = d₁ ^ k * a'
⊢ Associated (d₁ ^ k) a
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ ↑u * f.prod = f.prod * ↑u

Tactic:
mul_comm

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ f.prod * ↑u = f.prod * ↑u
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Fintype ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
have := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
    cases nonempty_fintype ι'
    -- We clean up a little:
    rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
    simp only [Cardinal.lift_natCast, Nat.cast_inj]
    -- Now we can use invariant basis number to show they have the same cardinality.
    apply card_eq_of_linearEquiv R
    exact
      (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
        Finsupp.linearEquivFunOnFinite R R ι'

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

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ Associated (normalize (Classical.choose ⋯) * lcm a b) (a * b)

Tactic:
mul_comm

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ Associated (lcm a b * normalize (Classical.choose ⋯)) (a * b)
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
f : α → α
hf : Function.Involutive f
⊢ Function.Involutive fun M ↦ M.map f

Tactic:
intro

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
f : α → α
hf : Function.Involutive f
x✝ : Matrix m n α
⊢ (fun M ↦ M.map f) ((fun M ↦ M.map f) x✝) = x✝
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ⨆ ι, #↑↑ι ≤ #ι

Tactic:
apply ciSup_le'

Goal state after:
case a
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ ∀ (i : { s // LinearIndepOn R id s }), #↑↑i ≤ #ι
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case intro
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
ι : Type w
h : Basis ι R M
val✝ : Fintype ι
⊢ ↑(finrank R M) = #ι

Tactic:
rw [Cardinal.mk_fintype, finrank_eq_card_basis h]

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

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι✝ : Type w
ι' : Type w'
inst✝ : StrongRankCondition R
ι : Type u_2
b : Basis ι R R
this✝ : #ι = ↑(finrank R R)
this : Subsingleton ι ∧ Nonempty ι
⊢ Unique ι

Tactic:
exact Nonempty.some ((unique_iff_subsingleton_and_nonempty _).2 this)

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
⊢ Module.rank R M < ℵ₀

Tactic:
by
  simp only [Module.rank_def]
  obtain ⟨S, hS⟩ := Module.finite_def.mp ‹_›
  exact (ciSup_le' fun i => linearIndependent_le_span_finset _ i.prop S hS).trans_lt
    natCast_lt_aleph0

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : AddCommMonoid α
inst✝ : CommMagma α
v w : m → α
⊢ ∑ i, v i * w i = ∑ i, w i * v i

Tactic:
mul_comm

Goal state after:
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: n : Type u_3
α : Type u_10
inst✝² : NonUnitalNonAssocCommSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
d₁ d₂ : n → α
⊢ (diagonal fun i ↦ d₁ i * d₂ i) = diagonal fun i ↦ d₂ i * d₁ i

Tactic:
mul_comm

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I

Tactic:
mul_comm

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : b * a ∈ I ^ n
⊢ a ∈ I ^ n ∨ b ∈ I
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝¹ : NonUnitalSemiring α
inst✝ : Fintype m
A : Matrix m m α
⊢ IsRightRegular A ↔ Function.Injective fun v ↦ v ᵥ* A

Tactic:
cases isEmpty_or_nonempty m
  · simp [IsRightRegular, Function.injective_of_subsingleton]
  exact mul_left_injective_iff_vecMul_injective

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ Finite ↑⋯.choose

Tactic:
infer_instance

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ∀ {w x y z : R}, f w = f x → f y = f z → f (w * y) = f (x * z)

Tactic:
intro

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ * y) = f (x * z)
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ∀ {w x y z : R}, f w = f x → f y = f z → f (w + y) = f (x + z)

Tactic:
intro

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ + y) = f (x + z)
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
convert! this h

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ s.ringCon x 0
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
⊢ ∃! c, u = c • LinearMap.id

Tactic:
by
    use c
    simp only [this, true_and]
    intro d hcd
    rw [LinearMap.ext_iff] at hcd
    simpa using (LinearEquiv.congr_arg (e := e.symm) (hcd (e 1))).symm

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ∀ (x : ι),
    ψ.comp (DFinsupp.singleAddHom (fun i ↦ β i) x) =
      (toAddMonoid fun i ↦ ψ.comp (of β i)).comp (DFinsupp.singleAddHom (fun i ↦ β i) x)

Tactic:
intro

Goal state after:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
x✝ : ι
⊢ ψ.comp (DFinsupp.singleAddHom (fun i ↦ β i) x✝) =
    (toAddMonoid fun i ↦ ψ.comp (of β i)).comp (DFinsupp.singleAddHom (fun i ↦ β i) x✝)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type u_1
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalNonAssocSemiring A
inst✝⁹ : Module R A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : FunLike F A B
inst✝⁵ : NonUnitalAlgHomClass F R A B
inst✝⁴ : IsScalarTower R A A
inst✝³ : SMulCommClass R A A
ι : Sort u_2
inst✝² : Nonempty ι
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
f : F
hf : Function.Injective ⇑f
S : ι → NonUnitalSubalgebra R A
⊢ NonUnitalSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalSubalgebra.map f (S i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ S)

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
have := NonUnitalSubsemiring.isMulCommutative_iSup dir

Goal state after:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : NonUnitalNonAssocSemiring A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
this : IsMulCommutative ↥(⨆ i, (S i).toNonUnitalSubsemiring)
⊢ IsMulCommutative ↥(⨆ i, S i)
Module: Mathlib.LinearAlgebra.DirectSum.TensorProduct

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
i : ι₁
x : M₁ i ⊗[R] M₂'
⊢ (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) x) = (rTensor M₂' (lof R ι₁ M₁ i)) x

Tactic:
induction x using TensorProduct.induction_on with
  | zero => simp
  | tmul x y => rw [← lof_eq_of S, directSumLeft_symm_lof_tmul, rTensor_tmul, lof_eq_of, lof_eq_of]
  | add x y h₁ h₂ => simp [h₁, h₂]

Goal state after:
Module: Mathlib.Data.Finite.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Finite α
inst✝ : Finite β
this✝ : Fintype α
this : Fintype β
⊢ Finite (α ⊕ β)

Tactic:
infer_instance

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
inst✝¹ : StarRing R
S : Type u_1
inst✝ : NonAssocSemiring S
⊢ Function.Involutive fun f ↦ (starRingEnd R).comp f

Tactic:
intro

Goal state after:
R : Type u
inst✝² : CommSemiring R
inst✝¹ : StarRing R
S : Type u_1
inst✝ : NonAssocSemiring S
x✝ : S →+* R
⊢ (fun f ↦ (starRingEnd R).comp f) ((fun f ↦ (starRingEnd R).comp f) x✝) = x✝
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : Mul R
inst✝¹ : StarMul R
x : R
inst✝ : IsStarNormal x
⊢ star (star x) * star x = star x * star (star x)

Tactic:
rw [star_star, star_comm_self']

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x y : A
⊢ ↑⟨⅟2 • (x + y + star (x + y)), ⋯⟩ = ↑(⟨⅟2 • (x + star x), ⋯⟩ + ⟨⅟2 • (y + star y), ⋯⟩)

Tactic:
simp [add_add_add_comm]

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

Goal state before:
pp: R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q) ((a * b) ⊗ₜ[R] (n ⊗ₜ[R] q)) = (b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q)

Tactic:
mul_comm

Goal state after:
R : Type uR
A : Type uA
N : Type uN
Q : Type uQ
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
n : N
q : Q
a b : A
⊢ (distribBaseChange R A N Q) ((b * a) ⊗ₜ[R] (n ⊗ₜ[R] q)) = (b • a) ⊗ₜ[R] n ⊗ₜ[A] (1 ⊗ₜ[R] q)
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
s✝ t : Subfield K
f : K →+* L
s : Subfield K
x : K
hx : x ∈ s.carrier
⊢ (f x)⁻¹ ∈ (Subring.map f s.toSubring).carrier

Tactic:
exact ⟨x⁻¹, s.inv_mem hx, map_inv₀ f x⟩

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
⊢ ∀ {a b : K},
    a ∈ {x | ∃ (hx : x ∈ closure s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ closure s), p x hx} → a * b ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
rintro _ _ ⟨_, hx⟩ ⟨_, hy⟩; exact ⟨_, mul _ _ _ _ hx hy⟩

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: case pos
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : dx = 0
⊢ nx / 0 + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}

Tactic:
div_zero,

Goal state after:
case pos
K✝ : Type u
L : Type v
M : Type w
inst✝³ : DivisionRing K✝
inst✝² : DivisionRing L
inst✝¹ : DivisionRing M
s✝¹ : Set K✝
K : Type u
inst✝ : Field K
s✝ : Subfield K
s : Set K
nx : K
hnx : nx ∈ Subring.closure s
dx : K
hdx : dx ∈ Subring.closure s
x_mem : nx / dx ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
ny : K
hny : ny ∈ Subring.closure s
dy : K
hdy : dy ∈ Subring.closure s
y_mem : ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
hx0 : dx = 0
⊢ 0 + ny / dy ∈ {z | ∃ x ∈ Subring.closure s, ∃ y ∈ Subring.closure s, x / y = z}
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
x : OreLocalization S R
⊢ x • 0 = 0

Tactic:
induction x with | _ r s
   =>  _ 

Goal state after:
case c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r : R
s : ↥S
⊢ (r /ₒ s) • 0 = 0