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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
⊢ ∃ y ∈ {a | ∀ (b : α), r b a → b < a}, a ≤ y

Tactic:
refine ⟨b, fun c hc ↦ ?_, hb⟩

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
⊢ c < b
Module: Mathlib.SetTheory.Cardinal.Cofinality.Basic

Goal state before:
pp: α γ : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder γ
f : α → γ
hf : StrictMono f
hf' : IsCofinal (range f)
⊢ cof α = cof γ

Tactic:
simpa using lift_cof_congr_of_strictMono hf hf'

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 < _b₂.1
h₂ : _b₁.2 ≤ _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2

pp: case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 ≤ _b₂.1
h₂ : _b₁.2 < _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2

Tactic:
· exact .inl ⟨smul_lt_smul_of_pos_left h₁ ha, smul_le_smul_of_nonneg_left h₂ ha.le⟩

Goal state after:
case inr
α : Type u_1
β : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β
γ : Type u_3
inst✝⁹ : Zero α
inst✝⁸ : PartialOrder α
inst✝⁷ : PartialOrder β
inst✝⁶ : PartialOrder γ
inst✝⁵ : Zero β
inst✝⁴ : Zero γ
inst✝³ : SMulWithZero α β
inst✝² : SMulWithZero α γ
inst✝¹ : PosSMulStrictMono α β
inst✝ : PosSMulStrictMono α γ
_a : α
ha : 0 < _a
_b₁ _b₂ : β × γ
h₁ : _b₁.1 ≤ _b₂.1
h₂ : _b₁.2 < _b₂.2
⊢ (_a • _b₁).1 < (_a • _b₂).1 ∧ (_a • _b₁).2 ≤ (_a • _b₂).2 ∨ (_a • _b₁).1 ≤ (_a • _b₂).1 ∧ (_a • _b₁).2 < (_a • _b₂).2
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ ⟨(typein r).toRelEmbedding x, ⋯⟩ < ⟨succ ((typein r).toRelEmbedding x), ⋯⟩

Tactic:
Subtype.mk_lt_mk,

Goal state after:
case h.convert_6
α : Type u_4
r : α → α → Prop
wo : IsWellOrder α r
h : ∀ a < type r, succ a < type r
x : α
⊢ (typein r).toRelEmbedding x < succ ((typein r).toRelEmbedding x)
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ lift.{max v w, u} (type r) = lift.{max u w, v} (type s) ↔ Nonempty (r ≃r s)

Tactic:
refine Quotient.eq'.trans ⟨?_, ?_⟩

Goal state after:
case refine_1
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ } →
    Nonempty (r ≃r s)

case refine_2
α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
⊢ Nonempty (r ≃r s) →
    isEquivalent
      { α := ULift.{max v w, u} { α := α, r := r, wo := inst✝¹ }.α,
        r := ULift.down ⁻¹'o { α := α, r := r, wo := inst✝¹ }.r, wo := ⋯ }
      { α := ULift.{max u w, v} { α := β, r := s, wo := inst✝ }.α,
        r := ULift.down ⁻¹'o { α := β, r := s, wo := inst✝ }.r, wo := ⋯ }
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: case mp
s : Set Ordinal.{u_3}
a : Ordinal.{u_3}
ha : a ∈ upperBounds ((fun x ↦ x + 1) '' s)
⊢ BddAbove s

Tactic:
exact ⟨a, fun b hb ↦ (lt_add_one _).le.trans (ha (mem_image_of_mem _ hb))⟩

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

Goal state before:
pp: case type
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
⊢ ¬c < type r * type s

Tactic:
| type α r β s
   => 

Goal state after:
case type
c : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
inst✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
inst✝ : IsWellOrder β s
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
⊢ ¬c < type r * type s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
⊢ 0 • a = a * ↑0

Tactic:
zero_nsmul,

Goal state after:
a : Ordinal.{u_4}
⊢ 0 = a * ↑0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: b : ℕ
⊢ b ^ 0 ≤ 0 + 1

Tactic:
Nat.pow_zero

Goal state after:
b : ℕ
⊢ 1 ≤ 0 + 1
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
rw [← mul_le_iff_le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]
      apply Nat.div_mul_le_self

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

Goal state before:
pp: case a
a c b : Ordinal.{u_1}
ha : 0 < a
hc : 0 < c
hca : c ≤ a ^ ω
d : Ordinal.{u_1}
hd : nfp (fun x ↦ a * x) (a ^ ω * b + c) = a ^ ω * d
this✝ : a ^ ω * b + c ≤ a ^ ω * d
this : b < d
⊢ succ b ≤ d

Tactic:
rwa [succ_le_iff]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case add_one
f : Ordinal.{u_1} → Ordinal.{u_1}
hf : IsNormal f
a : Ordinal.{u_1}
a✝ : a + 1 = a → (a + 1).cof ≤ (f (a + 1)).cof
⊢ (a + 1).cof ≤ (f (a + 1)).cof

Tactic:
| add_one a =>

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

Goal state before:
pp: case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ ⨆ i, ↑(f i) + 1 < (succ c).ord

Tactic:
rw [← card_le_iff]

Goal state after:
case le_cof_ord
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
hc₀ : ℵ₀ ≤ succ c
hc' : (succ c).ord.cof < succ c
f : ↑(Iio (succ c).ord.cof.ord) → ↑(Iio (succ c).ord)
hf : IsFundamentalSeq f
⊢ (⨆ i, ↑(f i) + 1).card ≤ c
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ #(α ≃ β) = 2 ^ #α

Tactic:
mk_equiv_of_lift_eq (lift_inj.mpr eq),

Goal state after:
α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ 2 ^ lift.{u, u} #α = 2 ^ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Finset α) = #α

Tactic:
by
  classical
  exact Eq.symm <|
    le_antisymm (mk_le_of_injective fun _ _ => Finset.singleton_inj.1) <|
      calc
        #(Finset α) ≤ #(List α) := mk_le_of_surjective List.toFinset_surjective
        _ = #α := mk_list_eq_mk α

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

Goal state before:
pp: case inl.inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j' : α i
x : δ ⟨i, j'⟩.fst ⟨i, j'⟩.snd
⊢ (single ⟨i, j'⟩ x) ⟨i, j'⟩ = (single j' x) j'

pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
hj : j' ≠ j
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = (single j x) j'

Tactic:
· rw [single_eq_same, single_eq_same]

Goal state after:
case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → DecidableEq (α i)
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x : δ ⟨i, j⟩.fst ⟨i, j⟩.snd
j' : α i
hj : j' ≠ j
⊢ (single ⟨i, j⟩ x) ⟨i, j'⟩ = (single j x) j'
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case inl.inl
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j' : α i
x : δ i j'
⊢ (single j' x) j' = (single ⟨i, j'⟩ x) ⟨i, j'⟩

pp: case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ (single j x) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩

Tactic:
· rw [single_eq_same, single_eq_same]

Goal state after:
case inl.inr
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → (j : α i) → Zero (δ i j)
inst✝ : (i : ι) → DecidableEq (α i)
i : ι
j : α i
x : δ i j
j' : α i
hj : j' ≠ j
⊢ (single j x) j' = (single ⟨i, j⟩ x) ⟨i, j'⟩
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inl
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
i : κ
x : β (h i)
⊢ (single (h i) x) (h i) = (single i x) i

pp: case inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = (single k x) i

Tactic:
· rw [single_eq_same, single_eq_same]

Goal state after:
case inr
ι : Type u
β : ι → Type v
κ : Type u_1
inst✝² : DecidableEq ι
inst✝¹ : DecidableEq κ
inst✝ : (i : ι) → Zero (β i)
h : κ → ι
hh : Function.Injective h
k : κ
x : β (h k)
i : κ
hik : i ≠ k
⊢ (single (h k) x) (h i) = (single k x) i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case some.inl
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
j : ι
x : α (some j)
⊢ (single j x) j = (single (some j) x) (some j)

pp: case some.inr
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
⊢ (single i x) j = (single (some i) x) (some j)

Tactic:
· rw [single_eq_same, single_eq_same]

Goal state after:
case some.inr
ι : Type u
α : Option ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
⊢ (single i x) j = (single (some i) x) (some j)
Module: Mathlib.LinearAlgebra.Dual.Defs

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Submodule R (Dual R M)
x : M
⊢ x ∈ Φ.dualCoannihilator ↔ ∀ φ ∈ Φ, φ x = 0

Tactic:
dualCoannihilator,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
Φ : Submodule R (Dual R M)
x : M
⊢ x ∈ comap (Dual.eval R M) Φ.dualAnnihilator ↔ ∀ φ ∈ Φ, φ x = 0
Module: Mathlib.LinearAlgebra.BilinearMap

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴² : Semiring R
inst✝⁴¹ : Semiring R₂
inst✝⁴⁰ : Semiring S
inst✝³⁹ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝³⁸ : AddCommMonoid M
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N
inst✝³⁵ : AddCommMonoid N₂
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid P₂
inst✝³² : AddCommMonoid Pₗ
inst✝³¹ : Module R M
inst✝³⁰ : Module R M₂
inst✝²⁹ : Module S N
inst✝²⁸ : Module S N₂
inst✝²⁷ : Module R₂ P
inst✝²⁶ : Module S₂ P
inst✝²⁵ : Module R P₂
inst✝²⁴ : Module S₂ P₂
inst✝²³ : Module R Pₗ
inst✝²² : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²¹ : AddCommGroup M'
inst✝²⁰ : AddCommGroup P'
inst✝¹⁹ : Module R M'
inst✝¹⁸ : Module R₂ P'
inst✝¹⁷ : Module S₂ P'
inst✝¹⁶ : SMulCommClass S₂ R₂ P
inst✝¹⁵ : SMulCommClass S R Pₗ
inst✝¹⁴ : SMulCommClass S₂ R₂ P'
inst✝¹³ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ (r' • 1) • (B m) x✝ = r' • (B m) x✝

Tactic:
smul_one_smul

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
S₂ : Type u_4
inst✝⁴² : Semiring R
inst✝⁴¹ : Semiring R₂
inst✝⁴⁰ : Semiring S
inst✝³⁹ : Semiring S₂
M : Type u_5
M₂ : Type u_6
N : Type u_7
N₂ : Type u_8
P : Type u_9
P₂ : Type u_10
Pₗ : Type u_11
inst✝³⁸ : AddCommMonoid M
inst✝³⁷ : AddCommMonoid M₂
inst✝³⁶ : AddCommMonoid N
inst✝³⁵ : AddCommMonoid N₂
inst✝³⁴ : AddCommMonoid P
inst✝³³ : AddCommMonoid P₂
inst✝³² : AddCommMonoid Pₗ
inst✝³¹ : Module R M
inst✝³⁰ : Module R M₂
inst✝²⁹ : Module S N
inst✝²⁸ : Module S N₂
inst✝²⁷ : Module R₂ P
inst✝²⁶ : Module S₂ P
inst✝²⁵ : Module R P₂
inst✝²⁴ : Module S₂ P₂
inst✝²³ : Module R Pₗ
inst✝²² : Module S Pₗ
M' : Type u_12
P' : Type u_13
inst✝²¹ : AddCommGroup M'
inst✝²⁰ : AddCommGroup P'
inst✝¹⁹ : Module R M'
inst✝¹⁸ : Module R₂ P'
inst✝¹⁷ : Module S₂ P'
inst✝¹⁶ : SMulCommClass S₂ R₂ P
inst✝¹⁵ : SMulCommClass S R Pₗ
inst✝¹⁴ : SMulCommClass S₂ R₂ P'
inst✝¹³ : SMulCommClass S₂ R P₂
ρ₁₂ : R →+* R₂
σ₁₂ : S →+* S₂
R' : Type u_14
S' : Type u_15
inst✝¹² : Semiring R'
inst✝¹¹ : Semiring S'
inst✝¹⁰ : Module R' M
inst✝⁹ : Module S' N
inst✝⁸ : Module R' Pₗ
inst✝⁷ : Module S' Pₗ
inst✝⁶ : SMulCommClass S' R' Pₗ
inst✝⁵ : SMul S' S
inst✝⁴ : IsScalarTower S' S N
inst✝³ : IsScalarTower S' S Pₗ
inst✝² : SMul R' R
inst✝¹ : IsScalarTower R' R M
inst✝ : IsScalarTower R' R Pₗ
B : M →ₗ[R] N →ₗ[S] Pₗ
r' : R'
m : M
x✝ : N
⊢ r' • (B m) x✝ = r' • (B m) x✝
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
⊢ (∀ (t : Finset ι) (g : ι → R), ↑t ⊆ {i, j} → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • f i = 0 → ∀ i ∈ t, g i = 0) ↔
    ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0

Tactic:
refine ⟨fun h c d hcd ↦ ?_, fun h t g ht hg0 h0 ↦ ?_⟩

Goal state after:
case refine_1
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (t : Finset ι) (g : ι → R), ↑t ⊆ {i, j} → (∀ i ∉ t, g i = 0) → ∑ i ∈ t, g i • f i = 0 → ∀ i ∈ t, g i = 0
c d : R
hcd : c • f i + d • f j = 0
⊢ c = 0 ∧ d = 0

case refine_2
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i j : ι
f : ι → M
hij : i ≠ j
h : ∀ (c d : R), c • f i + d • f j = 0 → c = 0 ∧ d = 0
t : Finset ι
g : ι → R
ht : ↑t ⊆ {i, j}
hg0 : ∀ i ∉ t, g i = 0
h0 : ∑ i ∈ t, g i • f i = 0
⊢ ∀ i ∈ t, g i = 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x * y).coeff g = y.coeff.sum fun h r ↦ x.coeff (g * h⁻¹) * r

Tactic:
classical rw [coeff_mul, Finsupp.sum_comm]; gcongr; simp +contextual [← eq_mul_inv_iff_mul_eq]

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

Goal state before:
pp: case refine_1.single
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ (lmapDomain R R u) (single i s) ∈ span R (Set.range fun x ↦ single (u x) 1)

Tactic:
lmapDomain_apply,

Goal state after:
case refine_1.single
α : Type u_1
R : Type u_5
inst✝ : Semiring R
β : Type u_7
u : α → β
i : α
s : R
⊢ mapDomain u (single i s) ∈ span R (Set.range fun x ↦ single (u x) 1)
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case inl
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s = ∅
⊢ #s ≤ #(s * s)

Tactic:
simp [card_le_card_mul_right, *]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s : Finset α
h✝ : s.Nonempty
⊢ #s ≤ #(s * s)

Tactic:
simp [card_le_card_mul_right, *]

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

Goal state before:
pp: case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ (n + 1) * p = p * X ^ (n + 1)

Tactic:
conv_lhs => rw [pow_succ]

Goal state after:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
ih : X ^ n * p = p * X ^ n
⊢ X ^ n * X * p = p * X ^ (n + 1)
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ AddSubmonoid.closure (⇑(toFinsuppIso R).symm.toAddEquiv '' {x | ∃ m r, x = single m r}) ≤
    AddSubmonoid.closure {p | ∃ n a, p = (monomial n) a}

Tactic:
refine AddSubmonoid.closure_mono (Set.image_subset_iff.2 ?_)

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ {x | ∃ m r, x = single m r} ⊆ ⇑(toFinsuppIso R).symm.toAddEquiv ⁻¹' {p | ∃ n a, p = (monomial n) a}
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.update n 0 = erase n p

Tactic:
by
  ext
  rw [coeff_update_apply, coeff_erase]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Invariant

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hq : ⟨x, hx⟩ ∈ Submodule.comap (LinearMap.restrict f hp) q
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)

Tactic:
Submodule.mem_comap,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p : Submodule R M
hp : p ∈ f.invtSubmodule
q : Submodule R ↥p
x : M
hx : x ∈ p
hq : (LinearMap.restrict f hp) ⟨x, hx⟩ ∈ q
hx' : ⟨x, hx⟩ ∈ ↑q
⊢ p.subtype ⟨x, hx⟩ ∈ Submodule.comap f (Submodule.map p.subtype q)
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
⊢ (φ ∘ₗ p.projectionOnto q hpq + ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range

Tactic:
apply range_add_le _ _ |>.trans

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
⊢ (φ ∘ₗ p.projectionOnto q hpq).range ⊔ (ψ ∘ₗ q.projectionOnto p ⋯).range ≤ φ.range ⊔ ψ.range
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: case snd
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
R₁ : Type u_7
inst✝² : CommRing R₁
inst✝¹ : Module R₁ E
inst✝ : Module R₁ F
p q : Submodule R₁ E
h : IsCompl p q
φ : (↥p →ₗ[R₁] F) × (↥q →ₗ[R₁] F)
x : ↥q
⊢ ((fun φ ↦ (φ.domRestrict p, φ.domRestrict q)) ((ofIsComplProd h).toFun φ)).2 x = φ.2 x

Tactic:
exact ofIsCompl_apply_right h x

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 : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ IsCompl p f.ker

Tactic:
rw [← codRestrict_ker h]
  exact isCompl_of_proj h.codRestrict_apply_cod

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 : Submodule R E
f : E →ₗ[R] E
h : IsProj p f
⊢ f = ↑(p.prodEquivOfIsCompl f.ker ⋯) ∘ₗ id.prodMap 0 ∘ₗ ↑(p.prodEquivOfIsCompl f.ker ⋯).symm

Tactic:
by
  rw [← LinearMap.comp_assoc, LinearEquiv.eq_comp_toLinearMap_symm]
  ext x
  · simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inl, coprod_apply, coe_subtype,
      map_zero, add_zero, h.map_id x x.2, prodMap_apply, id_apply]
  · simp only [coe_prodEquivOfIsCompl, comp_apply, coe_inr, coprod_apply, map_zero,
      coe_subtype, zero_add, map_coe_ker, prodMap_apply, zero_apply, add_zero]

Goal state after:
Module: Mathlib.Data.Rel

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = if Disjoint t₁ t₂ then ∅ else s ×ˢ u

Tactic:
split_ifs with hst

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = ∅

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t₁ t₂ : Set β
u : Set γ
inst✝ : Decidable (Disjoint t₁ t₂)
hst : ¬Disjoint t₁ t₂
⊢ s ×ˢ t₁ ○ t₂ ×ˢ u = s ×ˢ u
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2.inl
G : Type u
H : Type v
inst✝⁴ : Mul G
inst✝³ : Mul H
inst✝² : IsRightCancelMul G
inst✝¹ : LinearOrder G
inst✝ : MulLeftStrictMono G
A B : Finset G
hc : 1 < #(A ×ˢ B)
hA : A.Nonempty
hB : B.Nonempty
a0 : G
ha0 : a0 ∈ A
b0 : G
hb0 : b0 ∈ B
he0 : a0 * b0 = (A * B).max' ⋯
a1 : G
ha1 : a1 ∈ A
b1 : G
hb1 : b1 ∈ B
he1 : a1 * b1 = (A * B).min' ⋯
this : UniqueMul A B a0 b0
a b : G
ha : a ∈ A
hb : b ∈ B
he : a * b = (a1, b1).1 * (a1, b1).2
hl : b < b1
⊢ a = (a1, b1).1 ∧ b = (a1, b1).2

Tactic:
exact ((he1 ▸ mul_lt_mul_right hl a1).not_ge <| min'_le _ _ <| mul_mem_mul ha1 hb).elim

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

Goal state before:
pp: R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
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✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
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
hg : Surjective ⇑g
⊢ { l // l ∘ₗ f = LinearMap.id } ≃ { e // f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e }

Tactic:
refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (l.1.prod g) ?_), ?_⟩
    invFun := fun e ↦ ⟨fst R M P ∘ₗ e.1, ?_⟩
    left_inv := ?_
    right_inv := ?_ }
  · have h₁ : ∀ x, l.1 (f x) = x := LinearMap.congr_fun l.2
    have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
    constructor
    · intro x y e
      simp only [LinearMap.prod_apply, Function.prod_apply, Prod.mk.injEq] at e
      obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
      rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero]
    · rintro ⟨x, y⟩
      obtain ⟨y, rfl⟩ := hg y
      refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩
  · have h₁ : ∀ x, l.1 (f x) = x := LinearMap.congr_fun l.2
    have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
    constructor
    · rw [LinearEquiv.eq_toLinearMap_symm_comp]
      ext <;> simp [h₁, h₂]
    · ext; simp
  · rw [LinearMap.comp_assoc, (LinearEquiv.eq_toLinearMap_symm_comp _ _).mp e.2.1]; rfl
  · intro; ext; simp
  · rintro ⟨e, rfl, rfl⟩
    ext x <;> simp

Goal state after: