mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * (↑n' + 1) + ↑m
⊢ ↑n' + ↑1 ≤ ↑n

Tactic:
← ENat.natCast_add,

Goal state after:
case h₂
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
this : ↑p.length ≤ (↑m + 1) * (↑n' + 1) + ↑m
⊢ ↑(n' + 1) ≤ ↑n
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
⊢ (if P then x₁ else 0) ⊗ₜ[R] x₂ = if P then x₁ ⊗ₜ[R] x₂ else 0

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_7
N : Type u_8
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
x₁ : M
x₂ : N
P : Prop
inst✝ : Decidable P
⊢ (x₁ ⊗ₜ[R] if P then x₂ else 0) = if P then x₁ ⊗ₜ[R] x₂ else 0

Tactic:
split_ifs <;> simp

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime x z
H2 : x ∣ y * z
⊢ x ∣ y

Tactic:
let ⟨a, b, H⟩ := H1
  rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
  exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x) + z * (b * y)

Tactic:
apply dvd_add

Goal state after:
case h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x)

case h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_right_right

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

Goal state before:
pp: case a
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R A
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)

Tactic:
· refine mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => ?_)
    rw [Submodule.mem_map_equiv] at hm hn ⊢
    exact mul_mem_mul hn hm

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

Goal state before:
pp: case mp.inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
hI : ((map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)).IsPrime
h : map (RingHom.fst R S) I = ⊤
⊢ (∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = p.prod ⊤) ∨
    ∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = ⊤.prod p

Tactic:
right

Goal state after:
case mp.inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal (R × S)
hI : ((map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I)).IsPrime
h : map (RingHom.fst R S) I = ⊤
⊢ ∃ p, p.IsPrime ∧ (map (RingHom.fst R S) I).prod (map (RingHom.snd R S) I) = ⊤.prod p
Module: Mathlib.RingTheory.Ideal.Prod

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal I

Tactic:
rw [I.ideal_prod_eq, ← span_singleton_generator (I.map _),
      ← span_singleton_generator (I.map (RingHom.snd R S)), ← Ideal.span, ← Ideal.span,
      ← Ideal.span_prod (iff_of_true (by simp) (by simp)), Set.singleton_prod_singleton]

Goal state after:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal
    (Ideal.span {(generator (Ideal.map (RingHom.fst R S) I), generator (Ideal.map (RingHom.snd R S) I))})
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
P : Type u_7
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherian R M
inst✝ : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range = g.ker
⊢ ∀ (a : Submodule R N), Submodule.map (f.ker.liftQ f ⋯) (Submodule.comap (f.ker.liftQ f ⋯) a) = a ⊓ f.range

Tactic:
simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ]

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

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
inst✝ : RingHomClass F R S
s : Set (Ideal S)
⊢ ⨅ I ∈ s, comap f I = ⨅ I ∈ comap f '' s, I

Tactic:
rw [iInf_image]

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

Goal state before:
pp: case neg
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 ∣ z * (x * gcdA x y) + z * (y * gcdB x y)

Tactic:
apply dvd_add

Goal state after:
case neg.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 ∣ z * (x * gcdA x y)

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 ∣ z * (y * gcdB x y)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ map f (r • I) = f r • map f I

Tactic:
← Submodule.ideal_span_singleton_smul,

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
r : R
I : Ideal R
f : R →+* S
⊢ map f (span {r} • I) = f r • map f I
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime} → j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}

Tactic:
rintro ⟨hj, hj'⟩

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
hj : map f I ≤ j
hj' : j.IsPrime
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : { g // ker f ≤ ker g }
⊢ (fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g) = g

Tactic:
ext
    simp only [comp_apply, liftOfRightInverseAux_comp_apply]

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 α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a : α
a0 : ¬a = 0
⊢ normalize (Classical.choose ⋯) = 0

Tactic:
let := gcdMonoidOfGCD gcd gcd_dvd_left gcd_dvd_right dvd_gcd

Goal state after:
case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a : α
a0 : ¬a = 0
this : GCDMonoid α := gcdMonoidOfGCD gcd gcd_dvd_left gcd_dvd_right ⋯
⊢ normalize (Classical.choose ⋯) = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
⊢ normalize (if a = 0 then 0 else normalize (Classical.choose ⋯)) = if a = 0 then 0 else normalize (Classical.choose ⋯)

Tactic:
split_ifs <;> simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : IsBezout.gcd (f a) (s.gcd f) * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a

Tactic:
rw [← hxy, add_mul, mul_comm x, mul_comm y] at hu

Goal state after:
case insert
R : Type u
α : Type u_1
inst✝² : CommRing R
inst✝¹ : IsBezout R
inst✝ : NormalizedGCDMonoid R
f : α → R
a : α
s : Finset α
ha : a ∉ s
ih : ∃ g, s.gcd f = ∑ a ∈ s, f a * g a
x y : R
hxy : x * f a + y * s.gcd f = IsBezout.gcd (f a) (s.gcd f)
u : Rˣ
hu : f a * x * ↑u + s.gcd f * y * ↑u = GCDMonoid.gcd (f a) (s.gcd f)
⊢ ∃ g, (insert a s).gcd f = ∑ a ∈ insert a s, f a * g a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
ih : I ≤ f i ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
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)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
right

Goal state after:
case pos
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
ih : I ≤ f i ∨ I ≤ f b ∨ ∃ i ∈ t, I ≤ f i
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)
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inr
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✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
have : Infinite ι' := Infinite.of_injective f f.2

Goal state after:
case inr
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✝ : Infinite ι
w₁ : lift.{w', w} #ι ≤ lift.{w, w'} #ι'
f : ι ↪ ι'
this : Infinite ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ 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:
right

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
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ↑I ⊆ ↑(f a) ∪ ↑(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.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
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ↑I ⊆ ↑(f a) ∪ ↑(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:
right

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
Hb : ¬f b ≤ f i
Hi : ¬I ≤ f i
this : ¬I ⊓ f a ⊓ f b ⊓ t.inf f ≤ f i
r : R
hri : r ∉ ↑(f i)
hr : r ∈ ↑(t.inf f)
hrb : r ∈ ↑(f b)
hrI : r ∈ ↑I
hra : r ∈ ↑(f a)
HI : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
k : ι
hkt : k ∈ t
ih : I ≤ f k
⊢ ∃ 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
inst✝ : StrongRankCondition R
ι : Type v
v : Basis ι R M
this : Nontrivial R
⊢ LinearIndepOn R id (range ⇑v)

Tactic:
LinearIndepOn

Goal state after:
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
⊢ LinearIndependent R fun (x : ↑(range ⇑v)) ↦ id ↑x
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ Pi.single i x j * v j = 0

Tactic:
simp [Pi.single_eq_of_ne hij]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
x : α
i j : m
hij : j ≠ i
⊢ v j * Pi.single i x j = 0

Tactic:
simp [Pi.single_eq_of_ne hij]

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

Goal state before:
pp: R : Type u_10
inst✝ : NonUnitalNonAssocSemiring R
A B : Matrix (Fin 2) (Fin 2) R
⊢ (A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧
    (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧
      (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩ <;>
  · rw [Matrix.mul_apply, Finset.sum_fin_eq_sum_range, Finset.sum_range_succ, Finset.sum_range_succ]
    simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
⊢ single i j (a + b) = single i j a + single i j b

Tactic:
by
  ext
  simp only [single, of_apply]
  split_ifs with h <;> simp [h]

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

Goal state before:
pp: m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ (∑ i, single i i (f i)) j k = diagonal f j k

Tactic:
rw [sum_apply, diagonal_apply, Finset.sum_eq_single j]

Goal state after:
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ single j j (f j) j k = if j = k then f j else 0

case h₀
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ ∀ b ∈ Finset.univ, b ≠ j → single b b (f b) j k = 0

case h₁
m : Type u_2
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : AddCommMonoid α
inst✝ : Fintype m
f : m → α
j k : m
⊢ j ∉ Finset.univ → single j j (f j) j k = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (finsuppTotal ι M I v) (Finsupp.mapRange (fun r ↦ if h : r ∈ I then ⟨r, h⟩ else 0) ⋯ a) = a.sum fun i c ↦ c • v i

Tactic:
rw [finsuppTotal_apply, Finsupp.sum_mapRange_index]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ (a.sum fun a b ↦ ↑(if h : b ∈ I then ⟨b, h⟩ else 0) • v a) = a.sum fun i c ↦ c • v i

ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ∀ (a : ι), ↑0 • v a = 0
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
D : Type u_6
inst✝⁸ : CommSemiring A
inst✝⁷ : CommSemiring C
inst✝⁶ : CommSemiring D
inst✝⁵ : Algebra A C
inst✝⁴ : Algebra A D
inst✝³ : CommSemiring B
inst✝² : Algebra A B
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
f✝ f : C →ₐ[A] D
⊢ (fun fg ↦
        let x := fg.fst.toAlgebra;
        AlgHom.restrictScalars A fg.snd)
      ((fun f ↦ ⟨AlgHom.domRestrict B f, AlgHom.extendScalars B f⟩) f) =
    f

Tactic:
by
    dsimp only
    ext
    rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
x : n → α
y : m → α
⊢ x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x

Tactic:
rw [dotProduct_mulVec, dotProduct_comm, vecMul_transpose]

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

Goal state before:
pp: F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F K * Module.rank K A = Module.rank F A

Tactic:
convert! lift_rank_mul_lift_rank F K A

Goal state after:
case e'_2.e'_5
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F K = lift.{v, v} (Module.rank F K)

case e'_2.e'_6
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank K A = lift.{v, v} (Module.rank K A)

case e'_3
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F A = lift.{v, v} (Module.rank F A)
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ (DirectSum.id M ι) x = x default

Tactic:
← AddEquiv.eq_symm_apply,

Goal state after:
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x : ⨁ (x : ι), M
⊢ x = (DirectSum.id M ι).symm (x default)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
by
  simp [iInf]

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x : A) → x ∈ adjoin R s → Prop
mem : ∀ (x : A) (hx : x ∈ s), p x ⋯
algebraMap : ∀ (r : R), p ((Algebra.algebraMap R A) r) ⋯
add : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯
mul : ∀ (x y : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯
x : A
hx : x ∈ adjoin R s
⊢ ∀ {a b : A},
    a ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} →
      b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx} → a + b ∈ {x | ∃ (hx : x ∈ adjoin R s), p x hx}

Tactic:
by rintro _ _ ⟨_, hpx⟩ ⟨_, hpy⟩; exact ⟨_, add _ _ _ _ hpx hpy⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
ι : Type u_2
N : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (N i)
inst✝² : (i : ι) → Module R (N i)
P : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (P i)
inst✝ : (i : ι) → Module R (P i)
u : (i : ι) → N i ≃ₗ[R] P i
r : R
x : ⨁ (i : ι), N i
⊢ (congrAddEquiv fun i ↦ (u i).toAddEquiv).toFun (r • x) =
    (RingHom.id R) r • (congrAddEquiv fun i ↦ (u i).toAddEquiv).toFun x

Tactic:
exact (DirectSum.lmap (fun i ↦ (u i).toLinearMap)).map_smul r x

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
s : Set A
⊢ Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s

Tactic:
have (S : Set A) : S ≤ equalizer φ ψ ↔ Set.EqOn φ ψ S := Iff.rfl

Goal state after:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
φ ψ : A →ₐ[R] B
s : Set A
this : ∀ (S : Set A), S ⊆ ↑(φ.equalizer ψ) ↔ Set.EqOn (⇑φ) (⇑ψ) S
⊢ Set.EqOn ⇑φ ⇑ψ ↑(adjoin R s) ↔ Set.EqOn (⇑φ) (⇑ψ) s
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case single.single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0) = (if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0

Tactic:
split_ifs <;> simp

Goal state after: