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

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = k1 * (d * k2 / d)

Tactic:
mul_div_cancel_left₀ _ hd0,

Goal state after:
case inr.inr
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = k1 * k2
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
x✝² : R
x✝¹ : x✝² ∈ ⊤
x✝ : M
⊢ x✝ ∈ ⊥ → x✝² • x✝ = 0

Tactic:
rintro rfl; rw [smul_zero]

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
⊢ (sSup {N, P}).annihilator = N.annihilator ⊓ P.annihilator

Tactic:
sSup_eq_iSup,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N P : Submodule R M
⊢ (⨆ a ∈ {N, P}, a).annihilator = N.annihilator ⊓ P.annihilator
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ lcm ?m.33 = GCDMonoid.lcm a s.lcm

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.33

Tactic:
lcm_cons

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ GCDMonoid.lcm ?a (lcm ?s) = GCDMonoid.lcm a s.lcm

case a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ α

case s
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?a ::ₘ ?s
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Multiset α
⊢ s.gcd ≠ 0 ↔ ∃ x, x ∈ s ∧ x ≠ 0

Tactic:
simp [gcd_eq_zero_iff]

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
hxy : f a * y ∈ map f I
ha : f a = x
b : R
hb : f b = y
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
← hb,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hxy : f a * f b ∈ map f I
hb : f b = y
⊢ x ∈ map f I ∨ y ∈ map f I
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case refine_2
n : ℕ
⊢ (fun x ↦ x.out.natAbs) ((fun x ↦ Associates.mk ↑x) n) = n

Tactic:
dsimp only [Associates.out_mk]
    rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]

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 : β → α
⊢ s.gcd f ≠ 0 ↔ ∃ x ∈ s, f x ≠ 0

Tactic:
simp [gcd_eq_zero_iff]

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

Goal state before:
pp: case neg.zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a (b ^ 0) ∣ gcd a b ^ 0

Tactic:
pow_zero,

Goal state after:
case neg.zero
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
hg : ¬gcd a b = 0
⊢ gcd a 1 ∣ gcd a b ^ 0
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
⊢ (∃ p, Prime p) ↔ ∃ x, x ≠ 0 ∧ ¬IsUnit x

Tactic:
by
  refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_isUnit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩
  obtain ⟨f, hf, -⟩ := WfDvdMonoid.exists_irreducible_factor hxu hx₀
  exact ⟨f, UniqueFactorizationMonoid.irreducible_iff_prime.mp hf⟩

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : I ^ 0 ≤ P
hn : n = 0
⊢ I ≤ P

Tactic:
pow_zero,

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
h : 1 ≤ P
hn : n = 0
⊢ I ≤ P
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = gcd a b * e - gcd a b * (f * d)

Tactic:
← he,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ c = b - gcd a b * (f * d)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b ∣ c

pp: case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ b

Tactic:
· rcases h with ⟨d, hd⟩
    rcases gcd_dvd_right a b with ⟨e, he⟩
    rcases gcd_dvd_left a b with ⟨f, hf⟩
    use e - f * d
    rw [mul_sub, ← he, ← mul_assoc, ← hf, ← hd, sub_sub_cancel]

Goal state after:
case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ b
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ b = gcd a c * e + gcd a c * (f * d)

Tactic:
← he,

Goal state after:
case h
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : c = gcd a c * e
f : α
hf : a = gcd a c * f
⊢ b = c + gcd a c * (f * d)
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ⇑f
⊢ False

pp: case refine_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ⇑f
⊢ n ≤ m

Tactic:
· exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)

Goal state after:
case refine_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ⇑f
⊢ n ≤ m
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔
    ¬∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective ⇑f

Tactic:
push Not

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) ↔ ∃ n f, Injective ⇑f
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos.inr.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
h' : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
ih : I ≤ f b
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

pp: case pos.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
h' : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
· exact Or.inl ih

Goal state after:
case pos.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
h' : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
h' : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
ih : I ≤ f a
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

pp: case pos.inr.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
h' : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
ih : I ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

pp: case pos.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
h' : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
· exact Or.inl ih

Goal state after:
case pos.inr.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
h' : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
ih : I ≤ f i
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

case pos.inr.inr
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
h' : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
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
ι : Type w
inst✝ : StrongRankCondition R
v : ι → M
hv : LinearIndependent R v
⊢ Module.rank R ↥(span R (range v)) = #↑(range v)

Tactic:
have := nontrivial_of_invariantBasisNumber R
  rw [← Cardinal.lift_inj, ← (Basis.span hv).mk_eq_rank,
    Cardinal.mk_range_eq_of_injective (@LinearIndependent.injective ι R M v _ _ _ _ hv)]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔ ¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀

Tactic:
push Not

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n f, Injective ⇑f) ↔ ∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (¬∀ (n : ℕ), Module.rank R (Fin n → R) < ℵ₀) ↔ ¬∀ n > 0, 0 < finrank R (Fin n → R)

Tactic:
push Not

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (∃ n, ℵ₀ ≤ Module.rank R (Fin n → R)) ↔ ∃ n > 0, finrank R (Fin n → R) ≤ 0
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
v : n → α
x y : Matrix m n α
⊢ (x + y) *ᵥ v = x *ᵥ v + y *ᵥ v

Tactic:
by
    ext m
    apply add_dotProduct

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ b ∈ I ^ n

Tactic:
← hb,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = b
⊢ (c * a + i) * b ∈ I ^ n
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι × ι'
⊢ (b.smulTower c) ij = b ij.1 • c ij.2

Tactic:
obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I✝ I J : TwoSidedIdeal R
h :
  { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } I ≤
    { toFun := ringCon, invFun := ofRingCon, left_inv := ⋯, right_inv := ⋯ } J
x : R
hx : I.ringCon x 0
⊢ J.ringCon x 0

Tactic:
exact h hx

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
carrier : Set R
zero_mem : 0 ∈ carrier
add_mem : ∀ {x y : R}, x ∈ carrier → y ∈ carrier → x + y ∈ carrier
neg_mem : ∀ {x : R}, x ∈ carrier → -x ∈ carrier
mul_mem_left : ∀ {x y : R}, y ∈ carrier → x * y ∈ carrier
mul_mem_right : ∀ {x y : R}, x ∈ carrier → x * y ∈ carrier
a b c d : R
h1 : a - b ∈ carrier
h2 : c - d ∈ carrier
⊢ a * (c - d) + (a - b) * d ∈ carrier

Tactic:
exact add_mem (mul_mem_left h2) (mul_mem_right h1)

Goal state after:
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 := ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ s.ringCon x 0

Tactic:
rel_iff,

Goal state after:
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) ↔ x - 0 ∈ s
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ Subalgebra.map f (iInf s) = ⨅ i, Subalgebra.map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Sort u_1
inst✝ : Nonempty ι
f : A →ₐ[R] B
hf : Function.Injective ⇑f
s : ι → Subalgebra R A
⊢ ↑(Subalgebra.map f (iInf s)) = ↑(⨅ i, Subalgebra.map f (s i))
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ centralizer R s.centralizer.centralizer = centralizer R s

Tactic:
apply SetLike.coe_injective

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
⊢ ↑(centralizer R s.centralizer.centralizer) = ↑(centralizer R s)
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

Goal state after:
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))
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
| g p

Tactic:
← hs p

Goal state after:
R : Type u_1
inst✝⁶ : Semiring R
P : Type u_2
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
h : Projective R P
f : M →ₗ[R] N
g : P →ₗ[R] N
hf : Function.Surjective ⇑f
φ : (P →₀ R) →ₗ[R] M := linearCombination R fun p ↦ Function.surjInv hf (g p)
s : P →ₗ[R] P →₀ R
hs : Function.LeftInverse ⇑(linearCombination R id) ⇑s
p : P
| g ((linearCombination R id) (s p))
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
t : (ι →₀ M) ⊗[R] N
i : ι
⊢ ((finsuppLeft R S M N ι) t) i = (rTensor N (Finsupp.lapply i)) t

Tactic:
induction t with

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
t : M ⊗[R] (ι →₀ N)
i : ι
⊢ ((finsuppRight R S M N ι) t) i = (lTensor M (Finsupp.lapply i)) t

Tactic:
induction t with

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

Goal state before:
pp: case inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

Tactic:
obtain hj | rfl := ne_or_eq j j'

Goal state after:
case inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

case inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ single i j (single k l r) i j k' l' = single (i, k) (j, l) r (i, k') (j, l')
Module: Mathlib.LinearAlgebra.Matrix.ConjTranspose

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
i : m
j : n
a : α
⊢ (single i j a)ᴴ = single j i (star a)

Tactic:
change (single i j a).transpose.map starAddEquiv = single j i (star a)
  simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
M : o → Matrix m n α
N : o → Matrix n p α
⊢ (blockDiagonal fun k ↦ M k * N k) = blockDiagonal M * blockDiagonal N

Tactic:
ext ⟨i, k⟩ ⟨j, k'⟩
  simp only [blockDiagonal_apply, mul_apply, ← Finset.univ_product_univ, Finset.sum_product]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
β : Type u_13
inst✝² : DecidableEq o
inst✝¹ : Zero α
inst✝ : Zero β
M : (i : o) → Matrix (m' i) (n' i) α
f : α → β
hf : f 0 = 0
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ f (if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    if h : i✝.fst = j✝.fst then f (M i✝.fst i✝.snd (cast ⋯ j✝.snd)) else 0

Tactic:
rw [apply_dite f, hf]

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

Goal state before:
pp: case add
R : Type uR
A : Type uA
N : Type uN
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring A
inst✝² : Algebra R A
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
x y : A ⊗[A] (A ⊗[R] N)
hx : (cancelBaseChange R A A A N) x = (TensorProduct.lid A (A ⊗[R] N)) x
hy : (cancelBaseChange R A A A N) y = (TensorProduct.lid A (A ⊗[R] N)) y
⊢ (cancelBaseChange R A A A N) (x + y) = (TensorProduct.lid A (A ⊗[R] N)) (x + y)

Tactic:
simp [hx, hy]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
m : Type u_3
n : Type u_4
inst✝ : Fintype m
M : Matrix m n R
⊢ M.vecMulLinear.range = span R (Set.range M.row)

Tactic:
let := Classical.decEq m
  simp_rw [range_eq_map, ← iSup_range_single, Submodule.map_iSup, range_eq_map, ←
    Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
    Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion, iUnion_singleton_eq_range,
    LinearMap.single, LinearMap.coe_mk, AddHom.coe_mk, row_def]
  unfold vecMul
  simp_rw [single_dotProduct, one_mul]

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

Goal state before:
pp: K : Type u
L : Type v
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
ι : Sort u_1
inst✝ : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
K : Type u
L : Type v
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
ι : Sort u_1
inst✝ : Nonempty ι
f : K →+* L
s : ι → Subfield K
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
m : M
s : ↥S
⊢ f.mk' m s = 0 ↔ ∃ s, ↑s * m = 0

Tactic:
rw [← (f.map_units s).mul_left_inj, mk'_spec, zero_mul, map_eq_zero_iff]

Goal state after: