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

Goal state before:
pp: case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
b c : α
⊢ lcm 0 b ∣ c ↔ 0 ∣ c ∧ b ∣ c

pp: case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a c : α
⊢ lcm a 0 ∣ c ↔ a ∣ c ∧ 0 ∣ c

Tactic:
<;>

Goal state after:
case pos.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
b c : α
⊢ lcm 0 b ∣ c ↔ 0 ∣ c ∧ b ∣ c

case pos.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a c : α
⊢ lcm a 0 ∣ c ↔ a ∣ c ∧ 0 ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ gcd a b ∣ gcd a b

pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ gcd a b ∣ gcd a b

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ gcd a b ∣ gcd a b

case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
a b : α
⊢ gcd a b ∣ gcd a b
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ ∏ x ∈ s, x ∈ I ↔ ∃ p ∈ s, p ∈ I

Tactic:
rw [Finset.prod_eq_multiset_prod, Multiset.map_id']

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
hI : I.IsPrime
s : Finset R
⊢ s.val.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
hgcd : gcd = gcd
a b : α
⊢ lcm a b ∣ lcm a b

pp: case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
hgcd : gcd = gcd
a b : α
⊢ lcm a b ∣ lcm a b

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
hgcd : gcd = gcd
a b : α
⊢ lcm a b ∣ lcm a b

case refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
hgcd : gcd = gcd
a b : α
⊢ lcm a b ∣ lcm a b
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 ∣ gcd a c

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

Tactic:
<;>

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

case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ gcd a b
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 ∣ a ∧ gcd a b ∣ c

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

Tactic:
<;>

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

case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ a ∧ gcd a c ∣ b
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case succ
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
hp : ∀ i_1 ∈ insert i t, (f i_1).IsPrime
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
replace hp : IsPrime (f i) ∧ ∀ x ∈ t, IsPrime (f x) := (t.forall_mem_insert _ _).1 hp

Goal state after:
case succ
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
ih :
  ∀ {s : Finset ι} {a b : ι},
    (∀ i ∈ s, (f i).IsPrime) →
      s.card = n → ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
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
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : 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 : α
h✝ : a = 0
⊢ normalize 0 = 0

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 b : α
h✝ : ¬a = 0
⊢ normalize (normalize (Classical.choose ⋯)) = normalize (Classical.choose ⋯)

Tactic:
<;>

Goal state after:
case pos
α : 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 : α
h✝ : a = 0
⊢ normalize 0 = 0

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 b : α
h✝ : ¬a = 0
⊢ normalize (normalize (Classical.choose ⋯)) = normalize (Classical.choose ⋯)
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α → R) →ₗ[R] β → R
i : Injective ⇑f
P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)
Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
exact le_of_fin_injective R
    (Q.symm.toLinearMap ∘ₗ f ∘ₗ P) (Q.symm.injective.comp (i.comp P.injective))

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case mp
R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) → ∃ n f, Injective ⇑f

pp: case mpr
R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) → ∃ n f, Injective ⇑f

Tactic:
<;>

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) → ∃ n f, Injective ⇑f

case mpr
R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) → ∃ n f, Injective ⇑f
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ R ∙ x ≤ span {normalize x}

pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ span {normalize x} ≤ R ∙ x

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ R ∙ x ≤ span {normalize x}

case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : NormalizationMonoid R
x : R
inst✝ : (R ∙ x).IsPrincipal
⊢ span {normalize x} ≤ R ∙ x
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: R : Type u_7
m n : ℕ
A : Matrix (Fin m) (Fin n) R
i : Fin m
j : Fin n
⊢ ofArray (Array.ofFn fun k ↦ A k.divNat k.modNat) ⋯ i j = A i j

Tactic:
rw [ofArray_apply, Fin.getElem_fin, Array.getElem_ofFn, Fin.divNat_mkDivMod,
    Fin.modNat_mkDivMod]

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : P
⊢ dite P A B i j = if x : P then A x i j else B x i j

pp: case neg
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : ¬P
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
<;>

Goal state after:
case pos
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : P
⊢ dite P A B i j = if x : P then A x i j else B x i j

case neg
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
h : ¬P
⊢ dite P A B i j = if x : P then A x i j else B x i j
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : a = 0 ∧ b = 0
h✝ : a = 0 ∨ b = 0
⊢ Associated (0 * 0) (a * b)

pp: case neg
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : a = 0 ∧ b = 0
h✝ : ¬(a = 0 ∨ b = 0)
⊢ Associated (0 * 1) (a * b)

pp: case pos
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : ¬(a = 0 ∧ b = 0)
h✝ : a = 0 ∨ b = 0
⊢ Associated (1 * 0) (a * b)

pp: case neg
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : ¬(a = 0 ∧ b = 0)
h✝ : ¬(a = 0 ∨ b = 0)
⊢ Associated (1 * 1) (a * b)

Tactic:
<;>

Goal state after:
case pos
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : a = 0 ∧ b = 0
h✝ : a = 0 ∨ b = 0
⊢ Associated (0 * 0) (a * b)

case neg
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : a = 0 ∧ b = 0
h✝ : ¬(a = 0 ∨ b = 0)
⊢ Associated (0 * 1) (a * b)

case pos
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : ¬(a = 0 ∧ b = 0)
h✝ : a = 0 ∨ b = 0
⊢ Associated (1 * 0) (a * b)

case neg
α : Type u_1
G₀ : Type u_2
inst✝¹ : CommGroupWithZero G₀
inst✝ : DecidableEq G₀
a b : G₀
h✝¹ : ¬(a = 0 ∧ b = 0)
h✝ : ¬(a = 0 ∨ b = 0)
⊢ Associated (1 * 1) (a * b)
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

pp: case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

Tactic:
<;>

Goal state after:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i j : n
h : ¬i = j
⊢ (diagonal v)ᵀ i j = diagonal v i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j

pp: case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j

Tactic:
<;>

Goal state after:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ + diagonal d₂) i j = diagonal (fun i ↦ d₁ i + d₂ i) i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case pos
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

pp: case neg
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : ¬i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

Tactic:
<;>

Goal state after:
case pos
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j

case neg
n : Type u_3
R : Type u_7
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
d : n → α
i j : n
h : ¬i = j
⊢ diagonal (r • d) i j = (r • diagonal d) i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j

pp: case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : ¬i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j

Tactic:
<;>

Goal state after:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : NegZeroClass α
d : n → α
i j : n
h : ¬i = j
⊢ (-diagonal d) i j = diagonal (fun i ↦ -d i) i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i ↦ d₁ i - d₂ i) i j

pp: case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i ↦ d₁ i - d₂ i) i j

Tactic:
<;>

Goal state after:
case pos
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i ↦ d₁ i - d₂ i) i j

case neg
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : SubNegZeroMonoid α
d₁ d₂ : n → α
i j : n
h : ¬i = j
⊢ (diagonal d₁ - diagonal d₂) i j = diagonal (fun i ↦ d₁ i - d₂ i) i j
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case pos
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
h✝ : i✝ = j✝
⊢ f (d i✝) = f (d i✝)

pp: case neg
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
h✝ : ¬i✝ = j✝
⊢ f 0 = 0

Tactic:
<;>

Goal state after:
case pos
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
h✝ : i✝ = j✝
⊢ f (d i✝) = f (d i✝)

case neg
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
h✝ : ¬i✝ = j✝
⊢ f 0 = 0
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: case pos
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
h✝ : i✝ = j✝
⊢ f 1 = 1

pp: case neg
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
h✝ : ¬i✝ = j✝
⊢ f 0 = 0

Tactic:
<;>

Goal state after:
case pos
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
h✝ : i✝ = j✝
⊢ f 1 = 1

case neg
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
h✝ : ¬i✝ = j✝
⊢ f 0 = 0
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
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ finrank R M = 1

Tactic:
finrank_of_bijective_toSpanSingleton h

Goal state after:
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ 1 = 1
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
⊢ i ≠ a

pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
⊢ i ≠ b

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
⊢ i ≠ a

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hat : a ∉ insert b u
hp : ∀ i ∈ insert a (insert b u), i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a (insert b u)), ↑(f i)
has : a ∈ insert a (insert b u)
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
⊢ i ≠ b
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
hat : i ∉ insert b u
hp : ∀ i_1 ∈ insert i (insert b u), i_1 ≠ i → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i (insert b u)), ↑(f i_1)
has : i ∈ insert i (insert b u)
⊢ False

pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
u : Finset ι
i : ι
hiu : i ∈ u
hbu : i ∉ u
hat : a ∉ insert i u
hp : ∀ i_1 ∈ insert a (insert i u), i_1 ≠ a → i_1 ≠ i → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert a (insert i u)), ↑(f i_1)
has : a ∈ insert a (insert i u)
hbt : i ∈ insert i u
⊢ False

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
u : Finset ι
hbu : b ∉ u
hbt : b ∈ insert b u
i : ι
hiu : i ∈ u
hat : i ∉ insert b u
hp : ∀ i_1 ∈ insert i (insert b u), i_1 ≠ i → i_1 ≠ b → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert i (insert b u)), ↑(f i_1)
has : i ∈ insert i (insert b u)
⊢ False

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
u : Finset ι
i : ι
hiu : i ∈ u
hbu : i ∉ u
hat : a ∉ insert i u
hp : ∀ i_1 ∈ insert a (insert i u), i_1 ≠ a → i_1 ≠ i → (f i_1).IsPrime
h : ↑I ⊆ ⋃ i_1 ∈ ↑(insert a (insert i u)), ↑(f i_1)
has : a ∈ insert a (insert i u)
hbt : i ∈ insert i u
⊢ False
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ j ≠ a

pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ j ≠ b

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ j ≠ a

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
hbt : b ∉ t
j : ι
hj : j ∈ t
⊢ j ≠ b
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
j : ι
hj : j ∈ t
hat : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ j → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert j t), ↑(f i)
has : j ∈ insert j t
⊢ False

pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ j → (f i).IsPrime
hbt : j ∉ t
⊢ False

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
j : ι
hj : j ∈ t
hat : j ∉ t
hp : ∀ i ∈ insert j t, i ≠ j → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert j t), ↑(f i)
has : j ∈ insert j t
⊢ False

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a : ι
I : Ideal R
t : Finset ι
hat : a ∉ t
h : ↑I ⊆ ⋃ i ∈ ↑(insert a t), ↑(f i)
has : a ∈ insert a t
j : ι
hj : j ∈ t
hp : ∀ i ∈ insert a t, i ≠ a → i ≠ j → (f i).IsPrime
hbt : j ∉ t
⊢ False
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case e'_3
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ v i * w i = diagonal v i i * w i

pp: case convert_2
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ i ∉ Finset.univ → diagonal v i i * w i = 0

Tactic:
<;>

Goal state after:
case e'_3
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ v i * w i = diagonal v i i * w i

case convert_2
m : Type u_2
α : Type v
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonUnitalNonAssocSemiring α
v w : m → α
i : m
this : ∀ (j : m), j ≠ i → diagonal v i j * w j = 0
⊢ i ∉ Finset.univ → diagonal v i i * w i = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ j ≠ a

pp: case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ j ≠ b

Tactic:
<;>

Goal state after:
case refine_1
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ j ≠ a

case refine_2
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
a b : ι
I : Ideal R
t : Finset ι
hbt : b ∉ t
hp : ∀ i ∈ insert b t, i ≠ a → i ≠ b → (f i).IsPrime
h : ↑I ⊆ ⋃ i ∈ ↑(insert b t), ↑(f i)
has : a ∉ insert b t
hbs : b ∈ insert b t
j : ι
hj : j ∈ t
⊢ j ≠ b