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

Goal state before:
pp: case inr
a : Ordinal.{u_4}
ha : a ≠ 0
⊢ a % a = 0

Tactic:
· simp [mod_def, ha]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: o : Ordinal.{u_1}
ι : Sort u_2
f : ι → Ordinal.{u_1}
⊢ o * ⨆ i, f i = ⨆ i, o * f i

Tactic:
rw [← sSup_range, mul_sSup, ← Set.range_comp', sSup_range]

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case case1
b : ℕ
hb : 1 < b
x y : ℕ
h : 1 < b ∧ 1 < x
H₁ : b ^ (clog.go x b x).snd < x
H₂ : x ≤ b ^ ((clog.go x b x).snd + 1)
x✝ : (clog.go x b x).snd < y ∨ (clog.go x b x).snd ≥ y
⊢ (clog.go x b x).snd + 1 ≤ y ↔ x ≤ b ^ y

Tactic:
cases Nat.lt_or_ge (clog.go x b x).2 y with

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

Goal state before:
pp: case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ c ≤ a.card

Tactic:
rwa [add_one_of_aleph0_le] at ha

Goal state after:
case isSuccPrelimit
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
a : Ordinal.{u_1}
ha : c ≤ a.card + 1
⊢ ℵ₀ ≤ a.card
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inr
b n m : ℕ
h : n ≤ m
hb : 1 < b
⊢ clog b n ≤ clog b m

Tactic:
rw [clog_le_iff_le_pow hb]
    exact h.trans (le_pow_clog hb _)

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Exponential

Goal state before:
pp: case inr
b x c : Ordinal.{u_1}
hb : 1 < b
h : b ^ c ≤ x
hx : x ≠ 0
⊢ c ≤ log b x

Tactic:
· exact (opow_le_iff_le_log hb hx).1 h

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: a : Ordinal.{u_1}
⊢ deriv 0 a = a

Tactic:
by
  rw [deriv_zero, id_eq]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.FixedPoint

Goal state before:
pp: case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ nfp (fun x ↦ a * x) b ≤ a ^ ω

Tactic:
apply nfp_le_fp (isNormal_mul_right ha).monotone hba

Goal state after:
case inr.a
a b : Ordinal.{u_1}
hb : 0 < b
hba : b ≤ a ^ ω
ha : 0 < a
⊢ a * a ^ ω ≤ a ^ ω
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun x1 x2 ↦ x1 + x2) o
⊢ IsSuccLimit o

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]
  exact ⟨ho₁.ne_bot, fun _ ha ↦ ho ha ho₁⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Principal

Goal state before:
pp: case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ IsPrincipal (fun x1 x2 ↦ x1 + x2) o

Tactic:
isPrincipal_add_iff_add_self_lt,

Goal state after:
case inr
o : Ordinal.{u}
ho : IsPrincipal (fun x1 x2 ↦ x1 * x2) o
ho₂✝ : o ≠ 2
ho₂ : 2 < o
⊢ ∀ b < o, b + b < o
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #↑s < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup s < a

Tactic:
rw [← ord_lt_ord, sSup_ord]

Goal state after:
s : Set Cardinal.{u}
a : Cardinal.{u}
ha : #↑s < (Cardinal.lift.{u + 1, u} a).ord.cof
hs : ∀ i ∈ s, i < a
⊢ sSup (ord '' s) < a.ord
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: case hι
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ Cardinal.lift.{u, u + 1} #↑s ≤ Cardinal.lift.{u + 1, u} c

Tactic:
Cardinal.lift_id'.{u, u + 1}

Goal state after:
case hι
c : Cardinal.{u}
s : Set Ordinal.{u}
hs : #↑s ≤ Cardinal.lift.{u + 1, u} c
hs' : ∀ x ∈ s, x.card ≤ c
⊢ #↑s ≤ Cardinal.lift.{u + 1, u} c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
x✝ : 1 ≠ 0
⊢ StrictMono fun a ↦ ↑1 * a

Tactic:
simpa using! strictMono_id

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

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Uncountable β
⊢ ∃ a, Uncountable ↑(f ⁻¹' {a})

Tactic:
simp_rw [← Cardinal.aleph0_lt_mk_iff, ← aleph_one_le_iff]
  rcases lt_or_ge #α ℵ₀ with hα | hα
  · exact infinite_pigeonhole_card f ℵ₁ (by simp) aleph0_lt_aleph_one.le
      (by rw [isRegular_aleph_one.cof_ord]; exact hα.trans aleph0_lt_aleph_one)
  · obtain ⟨a, ha⟩ := infinite_pigeonhole_card_lt f h (aleph0_le_mk β)
    rw [← Order.succ_le_succ_iff, succ_aleph0] at hα
    exact ⟨a, hα.trans (succ_le_of_lt ha)⟩

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ ℵ_ ω ≤ c

Tactic:
by
  obtain ⟨o, rfl⟩ := mem_range_aleph_iff.2 hc.aleph0_le
  rw [isSingular_aleph_iff] at hc
  rw [aleph_le_aleph]
  exact omega0_le_of_isSuccLimit hc.1

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑↑s < #α

Tactic:
exact (finset_card_lt_aleph0 s).trans_le (aleph0_le_mk α)

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

Goal state before:
pp: case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #↑s = lift.{u, v} #↑t
val✝ : Fintype α
⊢ lift.{v, u} #↑sᶜ = lift.{u, v} #↑tᶜ

Tactic:
rcases lift_mk_eq'.1 h1 with ⟨e⟩

Goal state after:
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #↑s = lift.{u, v} #↑t
val✝ : Fintype α
e : α ≃ β
⊢ lift.{v, u} #↑sᶜ = lift.{u, v} #↑tᶜ
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ⨆ i, ⨆ (_ : p i), S i =
    AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p))

Tactic:
apply le_antisymm
  · refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
    rw [AddMonoidHom.comp_apply, filterAddMonoidHom_apply, filter_single_pos _ _ hi]
    exact sumAddHom_single _ _ _
  · rintro x ⟨v, rfl⟩
    refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
    refine AddSubmonoid.mem_iSup_of_mem i ?_
    by_cases hp : p i
    · simp [hp]
    · simp [hp]

Goal state after:
Module: Mathlib.Data.Fintype.Quotient

Goal state before:
pp: case a
ι : Type u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
S : (i : ι) → Setoid (α i)
l✝ : List ι
i : ι
l : List ι
C : ((i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)) → Prop
f : ∀ (a : (i_1 : ι) → i_1 ∈ i :: l → α i_1), C fun x1 x2 ↦ ⟦a x1 x2⟧
q : (i_1 : ι) → i_1 ∈ i :: l → Quotient (S i_1)
a : α i
as : (i : ι) → i ∈ l → α i
⊢ C fun j hj ↦ ⟦List.Pi.cons i l a as j hj⟧

Tactic:
exact f _

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝⁵ : DecidableEq ι
ι₁ : Type u₁
inst✝⁴ : DecidableEq ι₁
β₁ : ι₁ → Type v₁
inst✝³ : (i₁ : ι₁) → Zero (β₁ i₁)
inst✝² : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)
inst✝¹ : (i : ι) → AddCommMonoid (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i₁ : ι₁), β₁ i₁
g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i
⊢ (f.sum g).support ⊆ f.support.biUnion fun i ↦ (g i (f i)).support

Tactic:
have :
    ∀ i₁ : ι,
      (f.sum fun (i : ι₁) (b : β₁ i) => (g i b) i₁) ≠ 0 → ∃ i : ι₁, f i ≠ 0 ∧ ¬(g i (f i)) i₁ = 0 :=
    fun i₁ h =>
    let ⟨i, hi, Ne⟩ := Finset.exists_ne_zero_of_sum_ne_zero h
    ⟨i, mem_support_iff.1 hi, Ne⟩
  simpa [Finset.subset_iff, mem_support_iff, Finset.mem_biUnion, sum_apply] using this

Goal state after:
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ ⇑(∏ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∏ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∏ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∏ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
s : Finset ι
ψ : ι → AddChar A M
⊢ ⇑(∑ i ∈ s, ψ i) = ∏ i ∈ s, ⇑(ψ i)

Tactic:
induction s using Finset.cons_induction

Goal state after:
case empty
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
⊢ ⇑(∑ i ∈ ∅, ψ i) = ∏ i ∈ ∅, ⇑(ψ i)

case cons
ι : Type u_1
A : Type u_2
M : Type u_3
inst✝¹ : AddMonoid A
inst✝ : CommMonoid M
ψ : ι → AddChar A M
a✝¹ : ι
s✝ : Finset ι
h✝ : a✝¹ ∉ s✝
a✝ : ⇑(∑ i ∈ s✝, ψ i) = ∏ i ∈ s✝, ⇑(ψ i)
⊢ ⇑(∑ i ∈ cons a✝¹ s✝ h✝, ψ i) = ∏ i ∈ cons a✝¹ s✝ h✝, ⇑(ψ i)
Module: Mathlib.Algebra.Group.AddChar

Goal state before:
pp: A : Type u_1
M : Type u_2
inst✝¹ : AddGroup A
inst✝ : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) * ψ a = 1

Tactic:
simp only [← map_add_eq_mul, neg_add_cancel, map_zero_eq_one]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ f.coeff.sum single • v ∈ ↑W

Tactic:
Finsupp.sum,

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
G : Type u_6
inst✝⁵ : CommSemiring S
inst✝⁴ : Monoid M
V : Type u_7
inst✝³ : AddCommMonoid V
inst✝² : Module S V
inst✝¹ : Module S[M] V
inst✝ : IsScalarTower S S[M] V
W : Submodule S V
h : ∀ (g : M), ∀ v ∈ W, (of S M) g • v ∈ W
f : S[M]
v : V
hv : v ∈ ↑W
⊢ (∑ a ∈ f.coeff.support, single a (f.coeff a)) • v ∈ ↑W
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
b : β
inst✝ : DecidableEq α
s₁ s₂ : Finset α
hf : Injective fun a ↦ f a b
⊢ image₂ f (s₁ ∩ s₂) {b} = image₂ f s₁ {b} ∩ image₂ f s₂ {b}

Tactic:
simp_rw [image₂_singleton_right, image_inter _ _ hf]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (∑ a ∈ f.coeff.support, ∑ x ∈ g.coeff.support, if a * x = a0 * b0 then f.coeff a * g.coeff x else 0) =
    f.coeff a0 * g.coeff b0

Tactic:
← Finset.sum_product'

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (∑ x ∈ f.coeff.support ×ˢ g.coeff.support, if x.1 * x.2 = a0 * b0 then f.coeff x.1 * g.coeff x.2 else 0) =
    f.coeff a0 * g.coeff b0
Module: Mathlib.LinearAlgebra.Finsupp.Span

Goal state before:
pp: case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s t : Set α
hs : Disjoint s t
i : α
his : i ∉ s
⊢ (⨅ a ∈ sᶜ, (lapply a).ker) ⊓ ⨅ a ∈ tᶜ, (lapply a).ker ≤ (lapply i).ker

Tactic:
exact inf_le_of_left_le (iInf_le_of_le i <| iInf_le _ his)

Goal state after:
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
S₂ : Type u_2
inst✝³ : SMul S₁ S₂
inst✝² : SMulZeroClass S₁ R
inst✝¹ : SMulZeroClass S₂ R
inst✝ : IsScalarTower S₁ S₂ R
x✝ : S₁
y✝ : S₂
toFinsupp✝ : R[ℕ]
⊢ (x✝ • y✝) • { toFinsupp := toFinsupp✝ } = x✝ • y✝ • { toFinsupp := toFinsupp✝ }

Tactic:
simp_rw [← ofFinsupp_smul, smul_assoc]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ m ∈ ⨆ x, ↑x ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i

Tactic:
Submodule.mem_iSup_iff_exists_finset

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
S : Set (Submodule R M)
m : M
⊢ (∃ s, m ∈ ⨆ i ∈ s, ↑i) ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
c : R
h : c ≠ 0
⊢ (C c * X).support = {1}

Tactic:
by
  rw [C_mul_X_eq_monomial, support_monomial 1 h]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.support = {1}

Tactic:
← pow_one X,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ (X ^ 1).support = {1}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.coeffs = ∅ ↔ p = 0

Tactic:
by
  refine ⟨?_, fun h ↦ by simp [h]⟩
  contrapose!
  intro h
  rw [← support_nonempty] at h
  obtain ⟨n, hn⟩ := h
  rw [mem_support_iff] at hn
  exact ⟨p.coeff n, coeff_mem_coeffs hn⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case a.a
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
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ φ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case a.a
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
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
x : ↥p
⊢ φ x ∈ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case a
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
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
⊢ ψ.range ≤ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range

Tactic:
rintro - ⟨x, rfl⟩

Goal state after:
case a
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
p q : Submodule R E
hpq : IsCompl p q
φ : ↥p →ₗ[R] F
ψ : ↥q →ₗ[R] F
x : ↥q
⊢ ψ x ∈ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range
Module: Mathlib.Data.ENat.Lattice

Goal state before:
pp: s : Set ℕ∞
h : s.Infinite
⊢ sSup s = ⊤

Tactic:
by
  apply (sSup_eq_top ..).mpr
  intro x hx
  cases x with
  | top => simp at hx
  | coe x =>
    contrapose! h
    apply Finite.subset <| Finite.Set.finite_image {n : ℕ | n ≤ x} (fun (n : ℕ) => (n : ℕ∞))
    intro y hy
    specialize h y hy
    have hxt : y < ⊤ := lt_of_le_of_lt h hx
    use y.toNat
    simp [toNat_le_of_le_natCast h, LT.lt.ne_top hxt]

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
f : E →ₗ[R] F
g : E →ₗ[R] G
hf : f.range = ⊤
hg : g.range = ⊤
hfg : IsCompl f.ker g.ker
⊢ Function.Surjective ⇑(f.prod g)

Tactic:
rw [← range_eq_top]
      simp [range_prod_eq hfg.sup_eq_top, *]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ (∀ (x : E), ∃ y, q y = p x) ↔ ∀ ⦃x : M⦄, (∃ y, p y = x) → ∃ y, q y = x

Tactic:
forall_exists_index,

Goal state after:
S : Type u_5
inst✝⁴ : Semiring S
M : Type u_6
inst✝³ : AddCommMonoid M
inst✝² : Module S M
q : M →ₗ[S] M
hq : IsIdempotentElem q
E : Type u_7
inst✝¹ : AddCommMonoid E
inst✝ : Module S E
p : E →ₗ[S] M
⊢ (∀ (x : E), ∃ y, q y = p x) ↔ ∀ ⦃x : M⦄ (x_1 : E), p x_1 = x → ∃ y, q y = x
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
hg : Surjective ⇑g
⊢ [∃ l, g ∘ₗ l = LinearMap.id, ∃ l, l ∘ₗ f = LinearMap.id, ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE

Tactic:
tfae_have 1 ↔ 3 := by
    simpa using (h.splitSurjectiveEquiv hf).nonempty_congr

Goal state after:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst✝⁶ : Semiring 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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
hg : Surjective ⇑g
tfae_1_iff_3 : (∃ l, g ∘ₗ l = LinearMap.id) ↔ ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
⊢ [∃ l, g ∘ₗ l = LinearMap.id, ∃ l, l ∘ₗ f = LinearMap.id, ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e].TFAE
Module: Mathlib.Order.RelSeries

Goal state before:
pp: α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ (p.cons x hx).toList = x :: p.toList

Tactic:
cons,

Goal state after:
α : Type u_1
r : SetRel α α
p : RelSeries r
x : α
hx : (x, p.head) ∈ r
⊢ ((singleton r x).append p hx).toList = x :: p.toList
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ coheight a = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length

Tactic:
change height (α := αᵒᵈ) a = ⨆ (p : LTSeries α) (_ : p.head = a), ↑(p.length)

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ height a = ⨆ p, ⨆ (_ : RelSeries.head p = a), ↑p.length
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
⊢ map g (comap g r) ≤ map g q ↔ g.range ⊓ r ≤ map g q

Tactic:
map_comap_eq

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
⊢ g.range ⊓ r ≤ map g q ↔ g.range ⊓ r ≤ map g q
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, ∃ (b : StrictMono a.snd), (injStrictMono (Fintype.card α)) ⟨a, b⟩ = { length := l, toFun := f, step := mf }

Tactic:
use ⟨⟨l, bl⟩, f⟩, Fin.strictMono_iff_lt_succ.mpr mf

Goal state after:
case h
α : 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 α
⊢ (injStrictMono (Fintype.card α)) ⟨⟨⟨l, bl⟩, f⟩, ⋯⟩ = { length := l, toFun := f, step := mf }
Module: Mathlib.LinearAlgebra.TensorProduct.Defs

Goal state before:
pp: R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • (x + y) = r • (x + y) + s • (x + y)

Tactic:
simp_rw [TensorProduct.smul_add]

Goal state after:
R : Type u_1
R'' : Type u_5
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring R''
M : Type u_7
N : Type u_8
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R'' M
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : SMulCommClass R R'' M
r s : R''
x✝ : M ⊗[R] N
this : ∀ (r : R'') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
x y : M ⊗[R] N
ihx : (r + s) • x = r • x + s • x
ihy : (r + s) • y = r • y + s • y
⊢ (r + s) • x + (r + s) • y = r • x + r • y + (s • x + s • y)
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✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
r s : R'
x✝ x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
⊢ (r * s) • (x + y) = r • s • (x + y)

Tactic:
simp_rw [TensorProduct.smul_add]

Goal state after:
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✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
this : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ[R] n
r s : R'
x✝ x y : M ⊗[R] N
ihx : (r * s) • x = r • s • x
ihy : (r * s) • y = r • s • y
⊢ (r * s) • x + (r * s) • y = r • s • x + r • s • y
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
⊢ coheight x ≤ (↑m + 1) * coheight (f x) + ↑m

Tactic:
Order.coheight,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
x : α
⊢ height x ≤ (↑m + 1) * coheight (f x) + ↑m