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

Goal state before:
pp: s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
⊢ enumOrd t ≤ enumOrd s

Tactic:
by
  intro a
  rw [enumOrd, enumOrd]
  gcongr with b c
  exacts [enumOrd_nonempty hs a, enumOrd_le_of_subset hs hst c]

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

Goal state before:
pp: case h₂
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)

Tactic:
exact lt_mul_succ_div b hd

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

Goal state before:
pp: case inr
a b : Ordinal.{u_1}
h : a ≠ 0
⊢ a ^ (b + 1) = a ^ b * a

Tactic:
· rw [opow_of_ne_zero h, opow_of_ne_zero h]
    exact limitRecOn_add_one ..

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

Goal state before:
pp: a b c : Ordinal.{u_1}
h : b ≤ c
⊢ a ^ c = a ^ b * a ^ (c - b)

Tactic:
by rw [← opow_add, Ordinal.add_sub_cancel_of_le h]

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

Goal state before:
pp: a : Ordinal.{u_4}
⊢ IsSuccLimit a ↔ a ≠ 0 ∧ ω ∣ a

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_omega0_dvd]

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

Goal state before:

Tactic:
n ≤ c ^ clog c n := le_pow_clog hc _
    _ ≤ b ^ clog c n := Nat.pow_le_pow_left hb _

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

Goal state before:
pp: case pos
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
⊢ IsPrincipal op (sSup s)

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty
    · assumption
    simp only [IsPrincipal, lt_csSup_iff hs hs', forall_exists_index, and_imp]
    intro x y a has ha b hbs hb
    have h : max a b ∈ s := max_rec' _ has hbs
    exact ⟨_, h, H (max a b) h (lt_max_of_lt_left ha) (lt_max_of_lt_right hb)⟩

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.cof = 1 ↔ o ∈ range succ

Tactic:
by
  cases o using inductionOnWellOrder with | type α
  rw [cof_type, Order.cof_eq_one_iff, type_lt_mem_range_succ_iff]
  simp_rw [isTop_iff_isMax]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ preBeth o ≠ 0 ∧ (preBeth o).IsStrongPrelimit ↔ o ≠ 0 ∧ IsSuccPrelimit o

Tactic:
preBeth_eq_zero.ne,

Goal state after:
o : Ordinal.{u_1}
⊢ o ≠ 0 ∧ (preBeth o).IsStrongPrelimit ↔ o ≠ 0 ∧ IsSuccPrelimit o
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
ha : 1 < a
⊢ ℵ₀ ≤ o.cof

Tactic:
rwa [aleph0_le_cof_iff, ← ord_lt_ord, hf.ord_cof, ord_one]

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

Goal state before:
pp: ι : Type u
ι' : Type w
f : ι → Cardinal.{v}
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
hf : BddAbove (range f)
g : ι' → Cardinal.{v}
hg : BddAbove (range g)
⊢ (⨆ i, f i) + ⨆ j, g j = ⨆ i, ⨆ j, f i + g j

Tactic:
simp_rw [Cardinal.ciSup_add f hf, Cardinal.add_ciSup g hg]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℵ_ (o + 1)).IsRegular

Tactic:
rw [← succ_aleph]
  exact isRegular_succ (aleph0_le_aleph o)

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

Goal state before:
pp: c : Cardinal.{max u v}
ι : Type u
f : ι → Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hf : ∀ (i : ι), f i < c
⊢ sum f < c

Tactic:
apply (sum_le_lift_mk_mul_iSup _).trans_lt <|
    mul_lt_of_lt hc.1 hι (lift_iSup_lt_of_lt_cof_ord _ hf)
  rwa [lift_umax, c.lift_id', hc.cof_ord]

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

Goal state before:
pp: case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
left✝ : t ⊆ s
h2t : #↑t ≤ c
⊢ { toFun := fun t ↦ Subtype.val ⁻¹' ↑t, inj' := ⋯ } ⟨t, ⋯⟩ ∈ fun t ↦ Quot.lift ((fun α β ↦ Nonempty (α ↪ β)) ↑t) ⋯ c

Tactic:
exact (mk_preimage_of_injective _ _ Subtype.val_injective).trans h2t

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
apply extend_function.{u, v} f

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Goal state after:
case inl
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ i ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b i = 0

case inr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
b : β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
j : ι
hi : i ≠ j
⊢ j ∈ i ::ₘ ↑s ∨ Function.update (⇑f) i b j = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
⊢ (f.update i 0) j = (erase i f) j

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Goal state after:
case inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ (f.update i 0) i = (erase i f) i

case inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i j : ι
hi : i ≠ j
⊢ (f.update i 0) j = (erase i f) j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
⊢ p { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, ⋯⟩ }

Tactic:
have H3 : ∀ aux, (⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨i ::ₘ s, aux⟩⟩ : Π₀ i, β i) =
        ⟨fun j : ι => ite (j = i) 0 (f j), Trunc.mk ⟨s, H2⟩⟩ :=
      fun _ ↦ ext fun _ => rfl

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
p : (Π₀ (i : ι), β i) → Prop
h0 : p 0
ha : ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i), f i = 0 → b ≠ 0 → p f → p (single i b + f)
i : ι
s : Multiset ι
ih : ∀ (f : (i : ι) → β i) (H : ∀ (i : ι), i ∈ s ∨ f i = 0), p { toFun := f, support' := Trunc.mk ⟨s, H⟩ }
f : (i : ι) → β i
H : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ f i_1 = 0
H2 : ∀ (j : ι), j ∈ s ∨ (if j = i then 0 else f j) = 0
H3 :
  ∀ (aux : ∀ (i_1 : ι), i_1 ∈ i ::ₘ s ∨ (if i_1 = i then 0 else f i_1) = 0),
    { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, aux⟩ } =
      { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨s, H2⟩ }
⊢ p { toFun := fun j ↦ if j = i then 0 else f j, support' := Trunc.mk ⟨i ::ₘ s, ⋯⟩ }
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ i ∈ f.splitSupport.val ∨ f.split i = 0

Tactic:
← Finset.mem_def,

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ i ∈ f.splitSupport ∨ f.split i = 0
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
i : ι
⊢ f.split i ≠ 0 ∨ f.split i = 0

Tactic:
exact (em _).symm

Goal state after:
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: case pos
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : Zero N
n : N
i : ι
a b : η i
⊢ ((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) i) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) i) b

Tactic:
classical simp [split_apply, Finsupp.single_apply]

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

Goal state before:
pp: case refine_2.mk.refine_1
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
h : ∀ (i : ι), Function.Surjective (f i)
x : (i : ι) → β₂ i
support'✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ x i = 0 }
s : Multiset ι
hs : ∀ (i : ι), i ∈ s ∨ x i = 0
y : (i : ι) → β₁ i
hy : ∀ (i : ι), f i (y i) = x i ∧ (x i = 0 → y i = 0)
i : ι
⊢ i ∈ s ∨ y i = 0

Tactic:
exact (hs i).imp_right (hy i).2

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

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support

Tactic:
rcases eq_or_ne i j with (rfl | hi)

Goal state after:
case inl
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
⊢ i ∈ (f.update i b).support ↔ i ∈ insert i f.support

case inr
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
b : β i
h : b ≠ 0
j : ι
hi : i ≠ j
⊢ j ∈ (f.update i b).support ↔ j ∈ insert i f.support
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
m : Π₀ (i : ι), ↥(p i)
hm : ((lsum ℕ) fun i ↦ (p i).subtype) m = 0
i : ι
⊢ ((lsum ℕ) fun i ↦ (p i).subtype) (erase i m) = ↑(-m i)

Tactic:
rwa [← erase_add_single i m, map_add, lsum_single, Submodule.subtype_apply,
    add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm

Goal state after:
Module: Mathlib.Algebra.FreeAbelianGroup.Finsupp

Goal state before:
pp: X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ x ∈ (toFinsupp a).support ↔ (coeff x) a ≠ 0

Tactic:
Finsupp.mem_support_iff

Goal state after:
X : Type u_1
x : X
a : FreeAbelianGroup X
⊢ (toFinsupp a) x ≠ 0 ↔ (coeff x) a ≠ 0
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
p : γ → Prop
⊢ (∃ z ∈ image2 f ↑s ↑t, p z) ↔ ∃ x ∈ ↑s, ∃ y ∈ ↑t, p (f x y)

Tactic:
exists_mem_image2

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

Goal state before:
pp: ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
⊢ ∃ κ a, Injective a ∧ span K (range (v ∘ a)) = span K (range v) ∧ LinearIndependent K (v ∘ a)

Tactic:
have hs {i : ι} (hi : i ∈ s) : v i ∈ t := by obtain ⟨a, rfl⟩ := hi; simp [hf]

Goal state after:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ι → V
t : Set V
hsp : span K t = span K (range v)
hli : LinearIndependent K Subtype.val
f : ⦃a : V⦄ → a ∈ t → ι
hf : ∀ ⦃a : V⦄ (a_1 : a ∈ t), v (f a_1) = a
s : Set ι := range fun a ↦ f ⋯
hs : ∀ {i : ι}, i ∈ s → v i ∈ t
⊢ ∃ κ a, Injective a ∧ span K (range (v ∘ a)) = span K (range v) ∧ LinearIndependent K (v ∘ a)
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+ S
he : Injective ⇑f
⊢ Injective (map f)

Tactic:
by
  have : map (M := M) f = coeffEquiv.symm ∘ Finsupp.mapRange f (map_zero f) ∘ coeffEquiv := by
    ext; simp [ofCoeff_mapRange]
  simpa [this] using mapRange_injective _ (map_zero f) he

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
r : R
n : N
hn : n ∉ Set.range f
hf : Injective f
⊢ comapDomain f hf (single n r) = 0

Tactic:
ext; simp [*]

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
N : Type u_8
inst✝ : AddZeroClass N
f g : R[M] →+ N
hfg : ∀ (m : M), f.comp (singleAddHom m) = g.comp (singleAddHom m)
⊢ ∀ (m : M) (r : R), f (single m r) = g (single m r)

Tactic:
simpa [DFunLike.ext_iff] using hfg

Goal state after:
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun a b ↦ a ≤ b
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
⊢ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩ ≤ l.get i

Tactic:
exact (s.pairwise_sort (· ≤ ·)).rel_get_of_le (Nat.zero_le i)

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
n : ℕ
⊢ #(s ^ (n + 1)) ≤ #s ^ (n + 1)

Tactic:
by rw [pow_succ, pow_succ]; refine card_mul_le.trans (by gcongr; exact card_pow_le)

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 ↔ IsUnit s

Tactic:
by
  simp_rw [isUnit_iff, Set.isUnit_iff, coe_eq_singleton]

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

Goal state before:
pp: α : Type u_2
inst✝² : Mul α
inst✝¹ : IsRightCancelMul α
inst✝ : DecidableEq α
s t : Finset α
⊢ s.Nontrivial → t.Nonempty → (s * t).Nontrivial

Tactic:
by
  rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ p = 0

Tactic:
← one_smul R p,

Goal state after:
R : Type u
inst✝ : Semiring R
h : 0 = 1
p : R[X]
⊢ 1 • p = 0
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
inst✝ : UniqueProds G
A B : Finset G
hc : A.Nonempty ∧ B.Nonempty ∧ (1 < #A ∨ 1 < #B)
a : G
ha : a ∈ A
b : G
hb : b ∈ B
hu✝ : UniqueMul A B a b
C D : Finset G
hcard : 1 < #C ∨ 1 < #D
hC : 1 ∈ C
hD : 1 ∈ D
x✝ : Mul (Finset G) := Finset.mul
d1 : G
hd1 : d1 ∈ D
c2 : G
hc2 : c2 ∈ C
hc1 : 1 ∈ C
hd2 : 1 ∈ D
hu :
  ∀ ⦃a b : G⦄,
    (∃ y, (∃ a ∈ D, a⁻¹ = y) ∧ ∃ z ∈ C, y * z = a) →
      (∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = b) → a * b = d1⁻¹ * 1 * (1 * c2⁻¹) → a = d1⁻¹ * 1 ∧ b = 1 * c2⁻¹
h21 : c2 ≠ 1 ∨ d1 ≠ 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
refine ⟨c2, hc2, d1, hd1, h21, fun c4 d4 hc4 hd4 he => ?_⟩
        specialize hu ⟨_, ⟨_, hd4, rfl⟩, _, hC, rfl⟩ ⟨_, hD, _, ⟨_, hc4, rfl⟩, rfl⟩
        simpa only [mul_one, one_mul, ← mul_inv_rev, he, true_imp_iff, inv_inj, and_comm] using hu

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] ↥p
hf : ∀ (x : ↥p), f ↑x = x
x : E
hx : x ∈ p
⊢ x = ↑(f x)

Tactic:
rw [hf ⟨x, hx⟩, Subtype.coe_mk]

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

Goal state before:
pp: M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
comm₁₂ : f'.comp τ₁ = τ₂.comp f
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
⊢ MulExact ⇑f ⇑g ↔ MulExact ⇑f' ⇑g'

Tactic:
replace comm₁₂ := DFunLike.congr_fun comm₁₂

Goal state after:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
comm₂₃ : g'.comp τ₂ = τ₃.comp g
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), (f'.comp τ₁) x = (τ₂.comp f) x
⊢ MulExact ⇑f ⇑g ↔ MulExact ⇑f' ⇑g'
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
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)
⊢ ofIsCompl h (φ.1 + ψ.1) (φ.2 + ψ.2) = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2

Tactic:
ofIsCompl_add

Goal state after:
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)
⊢ ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2 = ofIsCompl h φ.1 φ.2 + ofIsCompl h ψ.1 ψ.2
Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case mp.mpr
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁵ : CommMonoid M₁
inst✝⁴ : CommMonoid M₂
inst✝³ : CommMonoid M₃
inst✝² : CommMonoid N₁
inst✝¹ : CommMonoid N₂
inst✝ : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective ⇑τ₁
h₂ : Bijective ⇑τ₂
h₃ : Injective ⇑τ₃
comm₁₂ : ∀ (x : M₁), f' (τ₁ x) = τ₂ (f x)
comm₂₃ : ∀ (x : M₂), g' (τ₂ x) = τ₃ (g x)
h : MulExact ⇑f ⇑g
x₂ : M₂
⊢ τ₂ x₂ ∈ Set.range ⇑f' → g' (τ₂ x₂) = 1

Tactic:
· rintro ⟨y₁, hy₁⟩
      obtain ⟨x₁, rfl⟩ := h₁ y₁
      rw [comm₂₃, (h x₂).2 _, map_one]
      exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩

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

Goal state before:
pp: ι : Sort u_2
f : ι → ℕ∞
a : ℕ∞
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
simp_rw [mul_comm, mul_iInf' h₀]

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

Goal state before:
pp: ι : Sort u_2
κ : Sort u_3
f : ι → ℕ∞
a : ℕ∞
p : ι → Prop
q : κ → Prop
hp : ∃ i, p i
hq : ∃ j, q j
g : κ → ℕ∞
h : ∀ (i : ι), p i → ∀ (j : κ), q j → f i + g j ≤ a
⊢ ⨆ i, ⨆ (_ : p i), ⨆ i_1, ⨆ (_ : q i_1), f i + g i_1 ≤ a

Tactic:
exact iSup₂_le fun i hi => iSup₂_le (h i hi)

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), p x ∈ q.range) ↔ p.range ≤ q.range

Tactic:
SetLike.le_def,

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), p x ∈ q.range) ↔ ∀ ⦃x : M⦄, x ∈ p.range → x ∈ q.range
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: R : Type u_1
inst✝² : CommRing 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 ⋯).conj (id.prodMap 0)

Tactic:
rw [LinearEquiv.conj_apply]
  exact h.eq_conj_prod_map'

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

Goal state before:
pp: case refine_2.right
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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g = snd R M P ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯).symm

Tactic:
rw [LinearEquiv.eq_comp_toLinearMap_symm]

Goal state after:
case refine_2.right
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
h : Exact ⇑f ⇑g
hf : Injective ⇑f
l : { l // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), g (↑l x) = x
h₂ : ∀ (x : M), g (f x) = 0
⊢ g ∘ₗ ↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + ↑l ∘ₗ snd R M P) ⋯) = snd R M P
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refine_2
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
⊢ UniqueMul A B (a1, b1).1 (a1, b1).2

Tactic:
· intro a b ha hb he
      obtain hl | rfl | hl := lt_trichotomy b b1
      · exact ((he1 ▸ mul_lt_mul_right hl a1).not_ge <| min'_le _ _ <| mul_mem_mul ha1 hb).elim
      · exact ⟨mul_right_cancel he, rfl⟩
      · exact ((he1 ▸ he ▸ mul_lt_mul_right hl a).not_ge <| min'_le _ _ <| mul_mem_mul ha hb1).elim

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case e'_4
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p : RelSeries r
i : Fin p.length
hi : ↑i + 1 ≤ p.length
⊢ i.castSucc.rev = ⟨p.length - (↑i + 1), ⋯⟩.succ

Tactic:
· ext
      simp only [Fin.val_rev, Fin.val_castSucc, Fin.val_succ]
      lia

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.toFun (i 0) = s.toFun 0

Tactic:
← hit,

Goal state after:
case refine_1
α : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
s : LTSeries α
h₁ : RelSeries.head s = ⊥
h₂ : RelSeries.last s = ⊤
t : RelSeries {(a, b) | a ⋖ b}
i : Fin (s.length + 1) ↪ Fin (t.length + 1)
hit : t.toFun ∘ ⇑i = s.toFun
hi₁ : i 0 = 0
hi₂ : i (Fin.last s.length) = Fin.last t.length
⊢ t.toFun (i 0) = (t.toFun ∘ ⇑i) 0