mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inl
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α = 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

pp: case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
· simp [ha]

Goal state after:
case inr
α : Type u_1
h : (#α).IsStrongPrelimit
ha : #α ≠ 0
⊢ #{ s // #↑s < (#α).ord.cof } = #α
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
⊢ False

Tactic:
let u : ∀ b, ∃ a, b ∈ f a := fun b => by simpa using (w.ge :) (Set.mem_univ b)

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
h : #↑(range f) < #β
u : ∀ (b : β), ∃ a, b ∈ f a :=
  fun b ↦
    Eq.mp (Eq.trans mem_iUnion._simp_1 (congrArg Exists (funext fun i ↦ SetLike.mem_coe._simp_1)))
      (Eq.ge w (mem_univ b))
⊢ False
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = #(α → β')

Tactic:
obtain ⟨e⟩ := lift_mk_eq'.mp leq
  have e₁ := lift_mk_eq'.mpr ⟨.equivCongr (.refl α) e⟩
  have e₂ := lift_mk_eq'.mpr ⟨.arrowCongr (.refl α) e⟩
  rw [lift_id'.{u, v}] at e₁ e₂
  rw [← e₁, ← e₂, lift_inj, mk_perm_eq_self_power, power_def]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
cases finite_or_infinite α
  · exact mk_le_aleph0.trans (le_max_left _ _)
  · rw [mk_list_eq_mk]
    apply le_max_right

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: case refine_3
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
φ : (i : ι) → ZeroHom (β i) γ
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
H1 : sx.toFinset ∩ sy.toFinset ⊆ sx.toFinset
H2 : sx.toFinset ∩ sy.toFinset ⊆ sy.toFinset
⊢ ∀ x ∈ sy.toFinset, x ∉ sx.toFinset ∩ sy.toFinset → (φ x) (f x) = 0

Tactic:
intro i H1 H2
        rw [Finset.mem_inter] at H2
        simp only [Multiset.mem_toFinset] at H1 H2
        convert! map_zero (φ i)
        exact (hx i).resolve_left (mt (fun H3 => And.intro H3 H1) H2)

Goal state after:
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
j : ι
x✝ : j ∈ sf.toFinset
hji : j ≠ i
⊢ (Pi.single i φ j) (f j) = 0

pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
hi : i ∉ sf.toFinset
⊢ (Pi.single i φ i) (f i) = 0

Tactic:
· simp [hji]

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : AddCommMonoid γ
i : ι
φ : ZeroHom (β i) γ
f : (i : ι) → β i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }
sf : Multiset ι
hf : ∀ (i : ι), i ∈ sf ∨ f i = 0
hi : i ∉ sf.toFinset
⊢ (Pi.single i φ i) (f i) = 0
Module: Mathlib.Data.DFinsupp.BigOperators

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
⊢ f.sum single = f

Tactic:
have := DFunLike.congr_fun (liftAddHom_singleAddHom (β := β)) f

Goal state after:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
this : (liftAddHom (singleAddHom β)) f = (AddMonoidHom.id (Π₀ (i : ι), β i)) f
⊢ f.sum single = f
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : LinearIndependent R ![x, y]
s t : R
h' : s • x = t • y
⊢ s = 0 ∧ t = 0

Tactic:
suffices H : s = 0 ∧ 0 = t from ⟨H.1, H.2.symm⟩
  exact h.eq_of_pair (by simpa using h')

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
⊢ Injective (Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩)

Tactic:
rintro (_ | _) (_ | _) eq

Goal state after:
case inl.inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑s
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝)
⊢ Sum.inl val✝¹ = Sum.inl val✝

case inl.inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ : ↑s
val✝ : ↑t
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝)
⊢ Sum.inl val✝¹ = Sum.inr val✝

case inr.inl
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ : ↑t
val✝ : ↑s
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inl val✝)
⊢ Sum.inr val✝¹ = Sum.inl val✝

case inr.inr
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
s : Set M
t : Set M'
hs : LinearIndependent R fun (x : ↑s) ↦ ↑x
ht : LinearIndependent R fun (x : ↑t) ↦ ↑x
a✝ : Nontrivial R
val✝¹ val✝ : ↑t
eq :
  Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝¹) =
    Sum.elim (fun i ↦ ⟨(inl R M M') ↑i, ⋯⟩) (fun i ↦ ⟨(inr R M M') ↑i, ⋯⟩) (Sum.inr val✝)
⊢ Sum.inr val✝¹ = Sum.inr val✝
Module: Mathlib.LinearAlgebra.DFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ ((lsum ℕ) fun i ↦ (p i).subtype).ker = ⊥

Tactic:
LinearMap.ker_eq_bot'

Goal state after:
ι : Type u_1
R : Type u_3
N : Type u_6
inst✝³ : DecidableEq ι
inst✝² : Ring R
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : ι → Submodule R N
h : ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) (erase i v) = ↑x → x = 0
⊢ ∀ (m : Π₀ (i : ι), ↥(p i)), ((lsum ℕ) fun i ↦ (p i).subtype) m = 0 → m = 0
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: case hs
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) fun i ↦ ⋃ i_1 ∈ i, f i_1

pp: case h
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ ∀ (i : Finset ι), LinearIndepOn R id (⋃ i_1 ∈ i, f i_1)

Tactic:
· apply directed_of_isDirected_le
    exact fun t₁ t₂ ht => iUnion_mono fun i => iUnion_subset_iUnion_const fun h => ht h

Goal state after:
case h
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → Set M
hl : ∀ (i : ι), LinearIndepOn R id (f i)
hd : ∀ (i : ι) (t : Set ι), t.Finite → i ∉ t → Disjoint (span R (f i)) (⨆ i ∈ t, span R (f i))
⊢ ∀ (i : Finset ι), LinearIndepOn R id (⋃ i_1 ∈ i, f i_1)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
⊢ Injective fun f ↦ ψ.compAddMonoidHom f

Tactic:
by
  rintro f g h
  rw [DFunLike.ext'_iff] at h ⊢; exact hψ.comp_left h

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NoZeroDivisors R
inst✝¹ : Mul A
inst✝ : UniqueProds A
a b : R[A]
hab : a.coeff.support.Nonempty ∧ b.coeff.support.Nonempty
da : A
a0 : da ∈ a.coeff.support
db : A
b0 : db ∈ b.coeff.support
h : UniqueMul a.coeff.support b.coeff.support da db
⊢ da * db ∈ (a * b).coeff.support

Tactic:
mem_support_iff

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NoZeroDivisors R
inst✝¹ : Mul A
inst✝ : UniqueProds A
a b : R[A]
hab : a.coeff.support.Nonempty ∧ b.coeff.support.Nonempty
da : A
a0 : a.coeff da ≠ 0
db : A
b0 : b.coeff db ≠ 0
h : UniqueMul a.coeff.support b.coeff.support da db
⊢ (a * b).coeff (da * db) ≠ 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommSemigroup M
f g : R[M]
⊢ f * g = g * f

Tactic:
simp [mul_def, Finsupp.sum, mul_comm, f.coeff.support.sum_comm]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : AddMonoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive (ofCoeff 0)

Tactic:
simpa using smul 0 (.of R M 1) (of 0)

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (map f A) (map f B) (f a0) (f b0) ↔ UniqueMul A B a0 b0

Tactic:
simp_rw [← mulHom_image_iff ⟨f, mul⟩ f.2, Finset.map_eq_image]

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Mul G
inst✝ : Mul H
A B : Finset G
a0 b0 : G
f : G ↪ H
mul : ∀ (x y : G), f (x * y) = f x * f y
⊢ UniqueMul (image (⇑f) A) (image (⇑f) B) (f a0) (f b0) ↔
    UniqueMul (image (⇑{ toFun := ⇑f, map_mul' := mul }) A) (image (⇑{ toFun := ⇑f, map_mul' := mul }) B)
      ({ toFun := ⇑f, map_mul' := mul } a0) ({ toFun := ⇑f, map_mul' := mul } b0)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
· rintro ⟨rfl, hn⟩
    exact empty_pow hn

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a

Tactic:
constructor
  · rintro ⟨u, rfl⟩
    obtain ⟨a, b, ha, hb, h⟩ := Finset.mul_eq_one_iff.1 u.mul_inv
    refine ⟨a, ha, ⟨a, b, h, singleton_injective ?_⟩, rfl⟩
    rw [← singleton_mul_singleton, ← ha, ← hb]
    exact u.inv_mul
  · rintro ⟨a, rfl, ha⟩
    exact ha.finset

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
a b : α
⊢ {b}.preimage (fun x ↦ a * x) ⋯ = {a⁻¹ * b}

Tactic:
classical rw [← image_mul_left', image_singleton]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u
inst✝ : Ring R
a b : R[ℕ]
⊢ { toFinsupp := a + -b } = { toFinsupp := a } - { toFinsupp := b }
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp - b.toFinsupp

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u
inst✝ : Ring R
a b : R[X]
⊢ (a - b).toFinsupp = a.toFinsupp + -b.toFinsupp
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : (fun x ↦ s • x) { toFinsupp := f } = (fun x ↦ s • x) { toFinsupp := g }
⊢ f = g

Tactic:
apply hs.isSMulRegular

Goal state after:
R : Type u
a b : R
m n : ℕ
inst✝³ : Semiring R
p q : R[X]
S : Type u_1
inst✝² : Semiring S
inst✝¹ : Module S R
inst✝ : IsTorsionFree S R
s : S
hs : IsRegular s
f g : R[ℕ]
hfg : (fun x ↦ s • x) { toFinsupp := f } = (fun x ↦ s • x) { toFinsupp := g }
⊢ (fun x ↦ s • x) f = (fun x ↦ s • x) g
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : n ∈ p.support
⊢ p.coeffs.Nonempty

Tactic:
mem_support_iff

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
hn : p.coeff n ≠ 0
⊢ p.coeffs.Nonempty
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) a + -(monomial n) b = (monomial n) a - (monomial n) b

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u
a b : R
inst✝ : Ring R
n : ℕ
⊢ (monomial n) a + -(monomial n) b = (monomial n) a + -(monomial n) b
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: case pos.refl
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x y : φ i
⊢ ((Finsupp.basis b).repr (single ⟨i, x⟩.fst ((b ⟨i, x⟩.fst) ⟨i, x⟩.snd))) ⟨i, y⟩ = (single ⟨i, x⟩ 1) ⟨i, y⟩

Tactic:
simp [Finsupp.single_apply_left sigma_mk_injective]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module R E
p q : Submodule R E
h : IsCompl p q
x : E
⊢ ((p.prodEquivOfIsCompl q h).symm x).1 = 0 ↔ x ∈ q

Tactic:
by
  conv_rhs => rw [← (prodEquivOfIsCompl p q h).apply_symm_apply x]
  rw [coe_prodEquivOfIsCompl', Submodule.add_mem_iff_left _ (Submodule.coe_mem _),
    mem_right_iff_eq_zero_of_disjoint h.disjoint]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝⁹ : Ring R
E : Type u_2
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module R E
F : Type u_3
inst✝⁶ : AddCommGroup F
inst✝⁵ : Module R F
G : Type u_4
inst✝⁴ : AddCommGroup G
inst✝³ : Module R G
p q : Submodule R E
S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
m : Submodule S M
h : IsCompl p q
x✝ : E
⊢ (((p.mkQ ∘ₗ q.subtype) ∘ₗ p.liftQ (q.projectionOnto p ⋯) ⋯) ∘ₗ p.mkQ) x✝ = (LinearMap.id ∘ₗ p.mkQ) x✝

Tactic:
simp [Quotient.eq, sub_mem_comm_iff, sub_projection_mem]

Goal state after:
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
⊢ ⨅ i, a * f i ≤ a * ⨅ i, f i

Tactic:
obtain ⟨b, hb⟩ := ENat.exists_eq_iInf f

Goal state after:
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
b : ι
hb : f b = ⨅ x, f x
⊢ ⨅ i, a * f i ≤ a * ⨅ i, f i
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, f i + iSup g ≤ a

Tactic:
add_iSup

Goal state after:
ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
inst✝¹ : Nonempty ι
inst✝ : Nonempty κ
g : κ → ℕ∞
h : ∀ (i : ι) (j : κ), f i + g j ≤ a
⊢ ⨆ i, ⨆ i_1, f i + g i_1 ≤ a
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ¬∃ i, a < f i
⊢ a - ⨆ i, f i = ⨅ i, a - f i

Tactic:
simp_rw [not_exists, not_lt] at h

Goal state after:
case inr
ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
inst✝ : Nonempty ι
ha : a ≠ ⊤
h : ∀ (x : ι), f x ≤ a
⊢ a - ⨆ i, f i = ⨅ i, a - f i
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 < ↑m
⊢ i.succ.castSucc.insertNth a p.toFun m.castSucc = p.toFun ⟨↑m - 1, ⋯⟩.castSucc

Tactic:
rw [Fin.insertNth_apply_above (h := hm)]

Goal state after:
case e'_3
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
a : α
prev_connect : (p.toFun i.castSucc, a) ∈ r
connect_next : (a, p.toFun i.succ) ∈ r
m : Fin (p.length + 1)
x : α := i.succ.castSucc.insertNth a p.toFun m.castSucc
y : α := i.succ.castSucc.insertNth a p.toFun m.succ
hm : ↑i + 1 < ↑m
⊢ ⋯ ▸ p.toFun (m.castSucc.pred ⋯) = p.toFun ⟨↑m - 1, ⋯⟩.castSucc
Module: Mathlib.Algebra.Algebra.NonUnitalHom

Goal state before:
pp: R : Type u
S : Type u₁
T : Type u_1
inst✝¹² : Monoid R
inst✝¹¹ : Monoid S
inst✝¹⁰ : Monoid T
φ : R →* S
A : Type v
B : Type w
C : Type w₁
inst✝⁹ : NonUnitalNonAssocSemiring A
inst✝⁸ : DistribMulAction R A
inst✝⁷ : NonUnitalNonAssocSemiring B
inst✝⁶ : DistribMulAction S B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : DistribMulAction T C
φ' : S →* R
ψ : S →* T
χ : R →* T
B₁ : Type u_2
inst✝³ : NonUnitalNonAssocSemiring B₁
inst✝² : DistribMulAction R B₁
inst✝¹ : DistribMulAction R B
inst✝ : DistribMulAction R C
f : A →ₙₐ[R] B
g : A →ₙₐ[R] C
⊢ Function.prod (⇑f) (⇑g) 0 = 0

Tactic:
simp only [Function.prod_apply, Prod.mk_zero_zero, map_zero]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (q.mapQ r g hqr).ker = comap q.mkQ (p.mapQ q f hpq).range ↔ g.range ⊓ r ≤ map g q

Tactic:
dsimp only [mapQ]

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact ⇑f ⇑g
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
hp : p.length ≠ 0
⊢ p.eraseLast.toList = p.toList.dropLast

Tactic:
apply List.ext_getElem
  · simpa using Nat.succ_pred_eq_of_ne_zero hp
  · intro i hi h2
    simp

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case zero
α : Type u_3
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : Fin (0 + 1) → α
h : ∀ (i : Fin 0), (s i.castSucc, s i.succ) ∈ {(a, b) | a < b}
⊢ ∃ t i,
    t.toFun ∘ ⇑i = { length := 0, toFun := s, step := h }.toFun ∧
      i 0 = 0 ∧ i (Fin.last { length := 0, toFun := s, step := h }.length) = Fin.last t.length

Tactic:
exact ⟨⟨0, s, nofun⟩, (Equiv.refl _).toEmbedding, rfl, rfl, rfl⟩

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α✝ : Type u_1
inst✝¹ : Preorder α✝
α : Type u_1
inst✝ : Preorder α
x : α
hfin : height x < ⊤
⊢ height x = ↑0 ↔ (0 = 0 ∨ ∃ y < x, height y = ↑0 - 1) ∧ ∀ y < x, height y < ↑0

Tactic:
simp [isMin_iff_forall_not_lt]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
R' : Type u_4
R'' : Type u_5
inst✝³⁸ : CommSemiring R
inst✝³⁷ : CommSemiring R₂
inst✝³⁶ : CommSemiring R₃
inst✝³⁵ : Monoid R'
inst✝³⁴ : Semiring R''
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
A : Type u_6
M : Type u_7
N : Type u_8
P : Type u_9
Q : Type u_10
S : Type u_11
M₂ : Type u_12
M₃ : Type u_13
N₂ : Type u_14
N₃ : Type u_15
P' : Type u_16
P₂ : Type u_17
P₃ : Type u_18
Q' : Type u_19
Q₂ : Type u_20
Q₃ : Type u_21
inst✝³³ : AddCommMonoid M
inst✝³² : AddCommMonoid N
inst✝³¹ : AddCommMonoid P
inst✝³⁰ : AddCommMonoid Q
inst✝²⁹ : AddCommMonoid S
inst✝²⁸ : AddCommMonoid P'
inst✝²⁷ : AddCommMonoid Q'
inst✝²⁶ : AddCommMonoid M₂
inst✝²⁵ : AddCommMonoid N₂
inst✝²⁴ : AddCommMonoid P₂
inst✝²³ : AddCommMonoid Q₂
inst✝²² : AddCommMonoid M₃
inst✝²¹ : AddCommMonoid N₃
inst✝²⁰ : AddCommMonoid P₃
inst✝¹⁹ : AddCommMonoid Q₃
inst✝¹⁸ : DistribMulAction R' M
inst✝¹⁷ : Module R'' M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module R N
inst✝¹⁴ : Module R S
inst✝¹³ : Module R P'
inst✝¹² : Module R Q'
inst✝¹¹ : Module R₂ M₂
inst✝¹⁰ : Module R₂ N₂
inst✝⁹ : Module R₂ P₂
inst✝⁸ : Module R₂ Q₂
inst✝⁷ : Module R₃ M₃
inst✝⁶ : Module R₃ N₃
inst✝⁵ : Module R₃ P₃
inst✝⁴ : Module R₃ Q₃
inst✝³ : SMul R' R
inst✝² : IsScalarTower R' R M
inst✝¹ : DistribMulAction R' N
inst✝ : IsScalarTower R' R N
r : R'
m : M
n : N
⊢ (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)

Tactic:
by
    conv_lhs => rw [← one_smul R m]
    conv_rhs => rw [← one_smul R n]
    rw [← smul_assoc, ← smul_assoc]
    exact Quotient.sound' <| AddConGen.Rel.of _ _ <| Eqv.of_smul _ _ _

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a, True ∧ (injStrictMono (Fintype.card α)) a = { length := l, toFun := f, step := mf }

Tactic:
true_and,

Goal state after:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Fintype α
inst✝ : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf : ∀ (i : Fin l), (f i.castSucc, f i.succ) ∈ {(a, b) | a < b}
bl : { length := l, toFun := f, step := mf }.length < Fintype.card α
⊢ ∃ a, (injStrictMono (Fintype.card α)) a = { length := l, toFun := f, step := mf }