mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case inl
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
this : single (u i) 1 = (lmapDomain R R u) (single i 1)
⊢ single i 1 =
    (LinearMap.linearProjOfIsCompl (span R (Set.range fun x ↦ single (v x) 1)) (lmapDomain R R u) ⋯ ⋯)
      ((lmapDomain R R u) (single i 1))

Tactic:
LinearMap.linearProjOfIsCompl_apply_left

Goal state after:
case inl
R : Type u_1
ι : Type u_3
inst✝ : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : α
this : single (u i) 1 = (lmapDomain R R u) (single i 1)
⊢ single i 1 = single i 1
Module: Mathlib.Order.RelSeries

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

Tactic:
exact hi

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4.e'_2
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
x : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.castSucc
y : Fin (p.length + 1 + (q.length + 1)) := Fin.cast ⋯ i.succ
hx : x = Fin.natAdd (p.length + 1) ⟨↑i - (p.length + 1), ⋯⟩
hy : y = Fin.natAdd (p.length + 1) ⟨↑i - p.length, ⋯⟩
⊢ p.length + 1 ≤ ↑i

Tactic:
exact hi

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ height (f x) = height x

Tactic:
apply le_antisymm
  · simpa using height_le_height_apply_of_strictMono _ f.symm.strictMono (f x)
  · exact height_le_height_apply_of_strictMono _ f.strictMono x

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ
hne : Nonempty { p // RelSeries.last p = a }
ha : ∀ (p : LTSeries α), RelSeries.last p = a → p.length ≠ n
⊢ ∀ y ∈ Set.range fun x ↦ (↑x).length, y ≤ n

Tactic:
rintro m ⟨⟨p, rfl⟩, hp⟩

Goal state after:
case h
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : (fun x ↦ (↑x).length) ⟨p, ⋯⟩ = m
⊢ m ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case h
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : (fun x ↦ (↑x).length) ⟨p, ⋯⟩ = m
⊢ m ≤ n

Tactic:
simp only at hp

Goal state after:
case h
α : Type u_1
inst✝ : Preorder α
n m : ℕ
p : LTSeries α
hne : Nonempty { p_1 // RelSeries.last p_1 = RelSeries.last p }
ha : ∀ (p_1 : LTSeries α), RelSeries.last p_1 = RelSeries.last p → p_1.length ≠ n
hp : p.length = m
⊢ m ≤ n
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : Preorder α
x : α
⊢ (∃ y, ∃ z < y, y < x) → 2 ≤ height x

Tactic:
rintro ⟨y, z, hzy, hyx⟩
    let p : LTSeries α := RelSeries.fromListIsChain [z, y, x] (List.cons_ne_nil z [y, x])
      (List.IsChain.cons_cons hzy <| List.isChain_pair.mpr hyx)
    have : p.last = x := by simp [p, ← RelSeries.getLast_toList]
    exact Order.length_le_height this.le

Goal state after:
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : IdemSemiring α
n : ℕ
nezero : n ≠ 0
⊢ ↑n = 1

Tactic:
rw [← Nat.one_le_iff_ne_zero] at nezero
  induction n, nezero using Nat.le_induction with
  | base => exact Nat.cast_one
  | succ x _ hx => rw [Nat.cast_add, hx, Nat.cast_one, add_idem 1]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : MulOneClass M
inst✝¹ : IsScalarTower R M M
inst✝ : SMulCommClass R M M
a : SubMulAction R M
x : M
⊢ x ∈ a → ∃ y ∈ a, ∃ a, a • y = x

Tactic:
· intro hx
      exact ⟨x, hx, 1, one_smul _ _⟩

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 y
H2 : IsCoprime x z
⊢ IsCoprime x (y * z)

Tactic:
isCoprime_comm

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : IsCoprime y x
H2 : IsCoprime z x
⊢ IsCoprime (y * z) x
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
isCoprime_comm

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime (y * z) x
⊢ IsCoprime y x
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
isCoprime_comm

Goal state after:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime (y + x * z) x
⊢ IsCoprime y x
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
isCoprime_comm

Goal state after:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + x * z) x
Module: Mathlib.RingTheory.Coprime.Basic

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

Tactic:
isCoprime_comm

Goal state after:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y + z * x) x
Module: Mathlib.RingTheory.Coprime.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime y x ↔ IsCoprime x y

Tactic:
isCoprime_comm

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : AddLeftMono R
x y : R
⊢ IsCoprime x y ↔ IsCoprime x y
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case insert.refine_3
R : Type u
I : Type v
inst✝ : CommSemiring R
z : R
s : I → R
t : Finset I
a : I
r : Finset I
har : a ∉ r
ih : (↑r).Pairwise (IsCoprime on s) → (∀ i ∈ r, s i ∣ z) → ∏ x ∈ r, s x ∣ z
Hs : (↑(insert a r)).Pairwise (IsCoprime on s)
Hs1 : ∀ i ∈ insert a r, s i ∣ z
⊢ ∏ x ∈ r, s x ∣ z

Tactic:
refine ih (Hs.mono ?_) fun i hi ↦ Hs1 i <| Finset.mem_insert_of_mem hi
      simp only [Finset.coe_insert, Set.subset_insert]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ Ideal.span s ≤ comap (LinearMap.toSpanSingleton R M x) M'

Tactic:
Ideal.span,

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
M' : Submodule R M
s : Set R
hs : Ideal.span s = ⊤
x : M
H : ∀ (r : ↑s), ↑r • x ∈ M'
⊢ span R s ≤ comap (LinearMap.toSpanSingleton R M x) M'
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
ha : f a = x
b : R
hb : f b = y
c : R
hc : c ∈ I
hc' : f c - f (a * b) = 0
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
← map_sub

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
hb : f b = y
c : R
hc : c ∈ I
hc' : f (c - a * b) = 0
⊢ x ∈ map f I ∨ y ∈ map f I
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
use -1, isUnit_one.neg
    rw [← neg_eq_iff_eq_neg.mpr h]
    simp only [neg_mul, one_mul]

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
x✝ : ∃ n f, Injective ⇑f
n : ℕ
f : (ℕ →₀ R) →ₗ[R] Fin n → R
inj : Injective ⇑f
⊢ ∃ f, Injective ⇑f

Tactic:
· exact ⟨f ∘ₗ Finsupp.lmapDomain R R (↑) ∘ₗ (Finsupp.linearEquivFunOnFinite ..).symm.toLinearMap,
      inj.comp <| by simpa using! Finsupp.mapDomain_injective Fin.val_injective⟩

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi fun x ↦ I
a b : ι → R
hab : a - b ∈ Ideal.pi fun x ↦ I
h : ι'
⊢ (e a - e b) h ∈ (fun x ↦ I) h

Tactic:
← map_sub

Goal state after:
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi fun x ↦ I
a b : ι → R
hab : a - b ∈ Ideal.pi fun x ↦ I
h : ι'
⊢ e (a - b) h ∈ (fun x ↦ I) h
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 : ℕ
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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1

Tactic:
have h' : (I : Set R) ⊆ f a ∪ f b ∪ ⋃ k ∈ (↑(insert i u) : Set ι), f k := by
        rw [Finset.coe_insert] at h ⊢
        rw [Finset.coe_insert] at h
        simp only [Set.biUnion_insert] at h ⊢
        rw [← Set.union_assoc (f i : Set R),
            Set.union_eq_self_of_subset_right hfji] at h
        exact h

Goal state after:
case pos
ι : 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 j : ι
hfji : f j ≤ f i
u : Finset ι
hju : j ∉ u
hit : i ∉ insert j u
hn : (insert j u).card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i (insert j u)), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ insert j u, (f x).IsPrime
hjt : j ∈ insert j u
hp' : ∀ k ∈ insert i u, (f k).IsPrime
hiu : i ∉ u
hn' : (insert i u).card = n
h' : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ k ∈ ↑(insert i u), ↑(f k)
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i (insert j u), I ≤ f i_1
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬{x | x ∈ S ∧ x ≠ 0}.Nonempty
a : R
⊢ a ∈ S ↔ a ∈ R ∙ 0

Tactic:
← @Submodule.bot_coe R R _ _ _,

Goal state after:
R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬{x | x ∈ S ∧ x ≠ 0}.Nonempty
a : R
⊢ a ∈ S ↔ a ∈ span R ↑⊥
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : 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 c : α
ac : a ∣ c
ab : a ∣ b
⊢ a ∣ normalize (if c = 0 then b else if b = 0 then c else Classical.choose ⋯)

Tactic:
split_ifs with h h_1
      · apply dvd_normalize_iff.2 ab
      · apply dvd_normalize_iff.2 ac
      have h0 : lcm c b ≠ 0 := lcm_ne_zero_iff.mpr ⟨h, h_1⟩
      rw [dvd_normalize_iff, ← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd c b)]
      rcases ab with ⟨d, rfl⟩
      rw [mul_eq_zero] at h_1
      push Not at h_1
      rw [mul_comm a, ← mul_assoc, mul_dvd_mul_iff_right h_1.1]
      apply lcm_dvd (Dvd.intro d rfl)
      rw [mul_comm, mul_dvd_mul_iff_right h_1.2]
      apply ac

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
i j : m
⊢ d default = of (fun x x_1 ↦ d default) default default

Tactic:
of_apply

Goal state after:
m : Type u_2
α : Type v
inst✝² : Unique m
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
i j : m
⊢ d default = d default
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
inst✝ : StrongRankCondition R
ι : Type w
b : Basis ι R M
κ : Type w
v : κ → M
i : LinearIndependent R v
val✝ : Fintype ι
this : Nontrivial R
⊢ #κ ≤ ↑(Fintype.card ↑(range ⇑b))

Tactic:
exact linearIndependent_le_span v i (range b) b.span_eq

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✝
R : Type u_2
M : Type u_3
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s t : Set M
inst✝ : Module.Finite R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ Fintype ↑(hs.extend hst)

Tactic:
refine Classical.choice (Cardinal.lt_aleph0_iff_fintype.1 ?_)

Goal state after:
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✝
R : Type u_2
M : Type u_3
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
s t : Set M
inst✝ : Module.Finite R ↥(span R t)
hs : LinearIndepOn R id s
hst : s ⊆ t
⊢ #↑(hs.extend hst) < ℵ₀
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case mp
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
h : x ∈ span K s
t : Finset M
ht_sub : ↑t ⊆ s
ht_card : t.card = finrank K ↥(span K s)
ht_span : span K ↑t = span K s
ht_indep : LinearIndepOn K id ↑t
⊢ ∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x

Tactic:
rcases mem_span_set.mp (ht_span ▸ h) with ⟨c, hct, hx⟩

Goal state after:
case mp
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
h : x ∈ span K s
t : Finset M
ht_sub : ↑t ⊆ s
ht_card : t.card = finrank K ↥(span K s)
ht_span : span K ↑t = span K s
ht_indep : LinearIndepOn K id ↑t
c : M →₀ K
hct : ↑c.support ⊆ ↑t
hx : (c.sum fun mi r ↦ r • mi) = x
⊢ ∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ single i j r (f (f.symm i)) (g j') = 0

Tactic:
single_apply_of_col_ne

Goal state after:
case inr.inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ 0 = 0

case inr.inl.hj
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_7
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : DecidableEq o
inst✝ : Zero α
f : l ≃ n
g : m ≃ o
i : n
j : o
r : α
j' : m
hj : g.symm j ≠ j'
⊢ j ≠ g j'
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
hp : ∀ I ∈ S, I = a ∨ I = b ∨ I.IsPrime
⊢ I ≠ ⊤

Tactic:
obtain rfl | rfl | hp := hp I mem

Goal state after:
case inl
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
b : Ideal R
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
ha : I ≠ ⊤
hp : ∀ I_1 ∈ S, I_1 = I ∨ I_1 = b ∨ I_1.IsPrime
⊢ I ≠ ⊤

case inr.inl
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a : Ideal R
ha : a ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
hb : I ≠ ⊤
hp : ∀ I_1 ∈ S, I_1 = a ∨ I_1 = I ∨ I_1.IsPrime
⊢ I ≠ ⊤

case inr.inr
R : Type u_2
inst✝¹ : CommRing R
M : Ideal R
inst✝ : M.IsMaximal
S : Set (Ideal R)
hs : S.Finite
a b : Ideal R
ha : a ≠ ⊤
hb : b ≠ ⊤
x✝ : ∃ i ∈ S, M ≤ i
I : Ideal R
mem : I ∈ S
le : M ≤ I
hp✝ : ∀ I ∈ S, I = a ∨ I = b ∨ I.IsPrime
hp : I.IsPrime
⊢ I ≠ ⊤
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α ≤ #(α →₀ β)

Tactic:
rw [← lift_id #(α →₀ β), ← lift_umax]

Goal state after:
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≤ #(α →₀ β)

Tactic:
rw [← lift_id #(α →₀ β), ← lift_umax]

Goal state after:
case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
Module: Mathlib.Data.Matrix.Basic

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
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
x : Matrix n n α
⊢ r • x = ((scalar n).comp (algebraMap R α)) r * x

Tactic:
by ext; simp [Matrix.scalar, Algebra.smul_def r]

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
x✝ y✝ : R
h : x✝ - y✝ ∈ carrier
⊢ y✝ - x✝ ∈ carrier

Tactic:
by simpa using neg_mem h

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

Goal state before:
pp: case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ ↑0 = ↑(if i = j then x else 0)

Tactic:
if_neg h.symm,

Goal state after:
case inr
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : ↥(A i)
h : j ≠ i
⊢ ↑0 = ↑0
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
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
⊢ (algebraMap R A) x ∈ ⋃₀ (SetLike.coe '' S)

Tactic:
obtain ⟨y, hy⟩ := hS

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' SetLike.coe '' S
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ (algebraMap R A) x ∈ ⋃₀ (SetLike.coe '' 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
f : A →ₐ[R] B
⊢ Subalgebra.toSubmodule (Subalgebra.map f ⊥) = Subalgebra.toSubmodule ⊥

Tactic:
by
    simpa only [Subalgebra.map_toSubmodule, toSubmodule_bot] using Submodule.map_one _

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R ↥(A i)
⊢ ⇑(h.collectedBasis v) = fun a ↦ ↑((v a.fst) a.snd)

Tactic:
simp [IsInternal.collectedBasis, coeLinearMap, DFinsupp.mapRange.linearEquiv,
    toModule, DFinsupp.lsum]

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_11
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
h : Function.Surjective ⇑(algebraMap R A)
a : A
m : M
n : N
⊢ (a • m) ⊗ₜ[R] n = m ⊗ₜ[R] (a • n)

Tactic:
obtain ⟨r, rfl⟩ := h a

Goal state after:
R : Type u_1
inst✝¹⁰ : CommSemiring R
M : Type u_5
N : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
A : Type u_11
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : Module A M
inst✝² : IsScalarTower R A M
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
h : Function.Surjective ⇑(algebraMap R A)
m : M
n : N
r : R
⊢ ((algebraMap R A) r • m) ⊗ₜ[R] n = m ⊗ₜ[R] ((algebraMap R A) r • n)
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
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ (linearCombination R id) ((g ∘ₗ i) x) = x

Tactic:
LinearMap.comp_apply,

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
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ (linearCombination R id) (g (i x)) = x
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
  | zero => simp
  | tmul m f => simp [finsuppRight_apply_tmul_apply]
  | add x y hx hy => simp [map_add, hx, hy]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
P : Type v
inst✝³ : AddCommMonoid P
inst✝² : Module R P
inst✝¹ : Small.{w, u} R
inst✝ : Small.{w, v} P
e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
  mapDomain.linearEquiv (Shrink.{w, u} R) R (equivShrink P).symm ≪≫ₗ mapRange.linearEquiv (Shrink.linearEquiv R R)
x✝ : Projective R P
i : P →ₗ[R] P →₀ R
hi : Function.LeftInverse ⇑(linearCombination R id) ⇑i
⊢ ∀ (x : P), (linearCombination R id) (i x) = LinearMap.id x

Tactic:
exact hi

Goal state after: