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

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
⊢ DirSupInacc s ↔ ∀ ⦃d : Set α⦄, d.Nonempty → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → (d ∩ s).Nonempty

Tactic:
simp [DirSupInacc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosReflectLE α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
smul : ∀ (a : α) (b : β), f (a • b) = a • f b
zero : f 0 = 0
b : β
hb : 0 < b
a₁ a₂ : α
h : a₁ • b ≤ a₂ • b
⊢ a₁ ≤ a₂

Tactic:
by
    simp only [← hf, ← lt_iff_lt_of_le_iff_le' hf hf, zero, smul] at *
    exact le_of_smul_le_smul_right h hb

Goal state after:
Module: Mathlib.Order.IsNormal

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
a : α
f : α → β
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ f a ∈ upperBounds (f '' s)

Tactic:
simpa [mem_upperBounds, hf.strictMono.le_iff_le] using hs.1

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

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
⊢ ∀ (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
    type r ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type r < univ.{u, v}

Tactic:
intro β

Goal state after:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
⊢ ∀ (r : β → β → Prop) [inst : IsWellOrder β r],
    type r ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type r < univ.{u, v}
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
⊢ typeLT Ordinal.{u_2} ≤ (cof Ordinal.{u_2}).ord

Tactic:
rw [type_lt_ordinal, ← ord_univ, ord_le_ord, le_cof_iff]

Goal state after:
α : Type u_1
⊢ ∀ (s : Set Ordinal.{u_2}), IsCofinal s → Cardinal.univ.{u_2, u_2 + 1} ≤ #↑s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ cof α ≤ #{ x // x ∈ s }

Tactic:
exact cof_le hs

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

Goal state before:
pp: case inl
a b c : Ordinal.{u_4}
h : a ≤ b + c
h' : b ≤ a
⊢ a - b ≤ c

Tactic:
rwa [← add_le_add_iff_left b, Ordinal.add_sub_cancel_of_le h']

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

Goal state before:
pp: s : Set Ordinal.{u}
inst✝ : Small.{u, u + 1} ↑s
a : Cardinal.{u}
ha : a ∈ upperBounds (succ ∘ card '' s)
b : Ordinal.{u}
hb : b ∈ s
⊢ b < a.ord

Tactic:
simpa [lt_ord] using ha (mem_image_of_mem _ hb)

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

Goal state before:
pp: a b : Ordinal.{u_4}
⊢ a * b = 0 ↔ a = 0 ∨ b = 0

Tactic:
induction a, b using inductionOn₂ with | _ α _ β _
  simp_rw [← type_prod_lex, type_eq_zero_iff_isEmpty, isEmpty_prod, iff_true_intro or_comm]

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

Goal state before:
pp: case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ ⨆ i, f i + 1 ≤ ⨆ i, f i

Tactic:
rw [ciSup_le_iff' (bddAbove_range_add_one_iff.2 hf')]

Goal state after:
case pos
β : Type u_3
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
f : β → Ordinal.{u}
hf : StrictMono f
hf' : BddAbove (range f)
⊢ ∀ (i : β), f i + 1 ≤ ⨆ i, f i
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
⊢ 1 ≤ o.card ↔ 1 ≤ o

Tactic:
by
  simpa using nat_le_card (n := 1)

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

Goal state before:
pp: b n : ℕ
hb : 1 < b
hn : n ≠ 0
⊢ log b n = log b (n + 1) ↔ b ^ log b (n + 1) ≠ n + 1

Tactic:
by
  rw [ne_eq, ← log_lt_log_succ_iff hb hn, not_lt]
  simp only [le_antisymm_iff, and_iff_right_iff_imp]
  exact fun _ ↦ log_monotone (le_add_right n 1)

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{max u v}
⊢ IsNormal f ↔
    (∀ (a : Ordinal.{u}), f a < f (succ a)) ∧ ∀ (o : Ordinal.{u}), IsSuccLimit o → (o.blsub fun x x_1 ↦ f x) = f o

Tactic:
rw [isNormal_iff_lt_succ_and_bsup_eq.{u, v}, and_congr_right_iff]
  intro h
  constructor <;> intro H o ho <;> have := H o ho <;>
    rwa [← bsup_eq_blsub_of_lt_succ_limit ho fun a _ => h a] at *

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

Goal state before:
pp: o : Ordinal.{u_4}
H : ∀ (n : ℕ), ↑n ≤ o
a : Ordinal.{u_4}
h : a < ω
⊢ a < o

Tactic:
let ⟨n, e⟩ := lt_omega0.1 h
      rw [e, ← succ_le_iff]; exact H (n + 1)

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

Goal state before:
pp: op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsPrincipal op (nfp (fun x ↦ ⨆ y, succ (op (↑y).1 (↑y).2)) o)

Tactic:
by
  intro a b ha hb
  rw [lt_nfp_iff] at *
  obtain ⟨m, ha⟩ := ha
  obtain ⟨n, hb⟩ := hb
  obtain h | h := le_total
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[m] o)
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[n] o)
  · use n + 1
    rw [Function.iterate_succ']
    apply (lt_succ _).trans_le
    exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod (ha.trans_le h) hb⟩
  · use m + 1
    rw [Function.iterate_succ']
    apply (lt_succ _).trans_le
    exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod ha (hb.trans_le h)⟩

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ∈ range ⇑ℵ_ ↔ ℵ₀ ≤ c

Tactic:
by
  rw [range_aleph, mem_Ici]

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

Goal state before:
pp: case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Function.Surjective (⇑ToType.mk ∘ fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩)

Tactic:
rw [EquivLike.comp_surjective]

Goal state after:
case neg
ι : Type u
f : ι → Ordinal.{v}
hf : BddAbove (range f)
⊢ Function.Surjective fun x ↦ ⟨↑x.snd.toOrd, ⋯⟩
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case a
a o : Ordinal.{u_1}
f : ↑(Iio a) → ↑(Iio o)
hf : IsFundamentalSeq f
⊢ o ≤ ⨆ i, ↑(f i) + 1

Tactic:
· refine le_of_forall_lt fun b hb ↦ ?_
    obtain ⟨_, ⟨c, rfl⟩, hc : b ≤ _⟩ := hf.isCofinal_range ⟨b, hb⟩
    apply hc.trans_lt
    rw [← add_one_le_iff]
    apply Ordinal.le_iSup

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

Goal state before:
pp: o : Ordinal.{u}
f : ↑(Iio o) → Ordinal.{max u v}
⊢ (⨆ a, f a).card ≤ sum fun i ↦ (f i.toOrd).card

Tactic:
apply le_of_eq_of_le (congr_arg _ _).symm (card_iSup_le_sum_card _)
  simpa using ToType.mk.symm.iSup_comp (g := fun x ↦ f x)

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

Goal state before:
pp: β : Type v
f : β → Cardinal.{u}
a : Cardinal.{u}
ha : Cardinal.lift.{u, v} #β < (Cardinal.lift.{v, u} a).ord.cof
hf : ∀ (i : β), f i < a
⊢ ⨆ i, f i < a

Tactic:
rw [← ord_lt_ord, iSup_ord]
  apply Ordinal.lift_iSup_lt_of_lt_cof <;> simpa

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

Goal state before:
pp: case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ lift.{v, u} 2 ≤ lift.{u, v} (c i)

Tactic:
lift_two,

Goal state after:
case a
ι : Type u
inst✝ : Infinite ι
c : ι → Cardinal.{v}
h₁ : ∀ (i : ι), 2 ≤ c i
h₂ : ∀ (i : ι), lift.{u, v} (c i) ≤ lift.{v, u} #ι
i : ι
⊢ 2 ≤ lift.{u, v} (c i)
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h₁ : ℵ₀ ≤ #β
h₂ : #α < (#β).ord.cof
x : α
h : #β ≤ #↑(f ⁻¹' {x})
⊢ ∃ p, #↑p = #↑(f ⁻¹' {x})

Tactic:
exact ⟨_, rfl⟩

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

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := (evalEquiv R M).symm g
⊢ f m = g f

Tactic:
rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]

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

Goal state before:
pp: ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ iSupIndep fun i ↦ (Finsupp.lsingle i).range

Tactic:
refine fun i ↦ disjoint_iff_inf_le.mpr ?_

Goal state after:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i : ι
⊢ (fun i ↦ (Finsupp.lsingle i).range) i ⊓ ⨆ j, ⨆ (_ : j ≠ i), (fun i ↦ (Finsupp.lsingle i).range) j ≤ ⊥
Module: Mathlib.Tactic.Module

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r₁ r₂ : R
x : M
l₁ l₂ l : NF R M
h : l₁.eval + l₂.eval = l.eval
⊢ ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

Tactic:
by
  simp only [← h, eval_cons, add_smul, add_assoc]
  congr! 1
  simp only [← add_assoc]
  congr! 1
  rw [add_comm]

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

Goal state before:
pp: case left
R : Type u_2
M : Type u_4
inst✝⁹ : Ring R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
x y : M
S : Type u_6
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : Module S R
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : IsScalarTower S R M
inst✝ : IsTorsionFree S R
a b c d : S
h : a * d ≠ b * c
s t : R
hst : s • (a • x + b • y) + t • (c • x + d • y) = 0
h₁ : a • s + c • t = 0
h₂ : b • s + d • t = 0
⊢ -(d • c • t) = (b * c) • s

Tactic:
rw [mul_comm, mul_smul, neg_eq_iff_add_eq_zero, add_comm, smul_comm d c, ← smul_add, h₂,
        smul_zero]

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
s : Set ι
a : ι
f : ι → V
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ (f a ∈ span K (f '' s) → a ∈ s)

Tactic:
by_cases has : a ∈ s
  · simp [insert_eq_of_mem has, has]
  simp [linearIndepOn_insert has, has]

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

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → β → γ
g : γ → δ
⊢ g '' image2 f ↑s ↑t = image2 (fun a b ↦ g (f a b)) ↑s ↑t

Tactic:
exact image_image2 _ _

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

Goal state before:
pp: α : Type u_1
β : Type u_3
δ : Type u_7
δ' : Type u_8
ε : Type u_9
inst✝² : DecidableEq δ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ ↑(image₂ f (image₂ g s t) u) = ↑(image₂ g' (image₂ f' s u) t)

Tactic:
by
    push_cast
    exact image2_right_comm h_right_comm

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

Goal state before:
pp: G : Type u
H : Type v
inst✝² : Mul G
inst✝¹ : Mul H
f : H →ₙ* G
hf : ∀ ⦃a b c d : H⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d
inst✝ : UniqueProds G
A B : Finset H
A0 : A.Nonempty
B0 : B.Nonempty
⊢ ∃ a0 ∈ A, ∃ b0 ∈ B, UniqueMul A B a0 b0

Tactic:
classical
    obtain ⟨a0, ha0, b0, hb0, h⟩ := uniqueMul_of_nonempty (A0.image f) (B0.image f)
    obtain ⟨a', ha', rfl⟩ := mem_image.mp ha0
    obtain ⟨b', hb', rfl⟩ := mem_image.mp hb0
    exact ⟨a', ha', b', hb', UniqueMul.of_mulHom_image f hf h⟩

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

Goal state before:
pp: case refine_3
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
f : G
hf : ∃ y ∈ D, ∃ z, (∃ a ∈ C, a⁻¹ = z) ∧ y * z = f
d1 : G
hd1 : d1 ∈ D
c1 : G
hc1 : c1 ∈ C
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⁻¹ * c1 * f → a = d1⁻¹ * c1 ∧ b = f
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
obtain ⟨d2, hd2, _, ⟨c2, hc2, rfl⟩, rfl⟩ := hf

Goal state after:
case refine_3
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
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
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⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
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
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
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⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
h12 : c1 ≠ 1 ∨ d2 ≠ 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

pp: case neg
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
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
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⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
h12 : c1 = 1 ∧ d2 = 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d

Tactic:
· refine ⟨c1, hc1, d2, hd2, h12, fun c3 d3 hc3 hd3 he => ?_⟩
        specialize hu ⟨_, ⟨_, hd1, rfl⟩, _, hc3, rfl⟩ ⟨_, hd3, _, ⟨_, hc2, rfl⟩, rfl⟩
        rw [mul_left_cancel_iff, mul_right_cancel_iff,
            mul_assoc, ← mul_assoc c3, he, mul_assoc, mul_assoc] at hu; exact hu rfl

Goal state after:
case neg
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
c1 : G
hc1 : c1 ∈ C
d2 : G
hd2 : d2 ∈ D
c2 : G
hc2 : c2 ∈ C
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⁻¹ * c1 * (d2 * c2⁻¹) → a = d1⁻¹ * c1 ∧ b = d2 * c2⁻¹
h12 : c1 = 1 ∧ d2 = 1
⊢ ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this : IsCompl (span R (⇑Finsupp.basisSingleOne '' Set.range u)) (span R (⇑Finsupp.basisSingleOne '' Set.range v))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))

Tactic:
← Set.range_comp,

Goal state after:
R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this : IsCompl (span R (Set.range (⇑Finsupp.basisSingleOne ∘ u))) (span R (⇑Finsupp.basisSingleOne '' Set.range v))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))
Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace

Goal state before:
pp: R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this : IsCompl (span R (Set.range (⇑Finsupp.basisSingleOne ∘ u))) (span R (⇑Finsupp.basisSingleOne '' Set.range v))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))

Tactic:
← Set.range_comp,

Goal state after:
R : Type u_1
ι : Type u_3
inst✝ : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this : IsCompl (span R (Set.range (⇑Finsupp.basisSingleOne ∘ u))) (span R (Set.range (⇑Finsupp.basisSingleOne ∘ v)))
⊢ IsCompl (span R (Set.range fun x ↦ single (u x) 1)) (span R (Set.range fun x ↦ single (v x) 1))
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case inr.inl
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯)
        (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).castSucc,
      (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯)
        (Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length)).succ) ∈
    r

pp: case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc, (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ) ∈ r

Tactic:
· convert! connect
      · convert! Fin.append_left p q _
      · convert! Fin.append_right p q _; rfl

Goal state after:
case inr.inr
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : (p.last, q.head) ∈ r
i : Fin (p.length + q.length + 1)
hi : Fin.castLE (@RelSeries.append._proof_3 α r p q) (Fin.last p.length) < i
⊢ ((Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.castSucc, (Fin.append p.toFun q.toFun ∘ Fin.cast ⋯) i.succ) ∈ r
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✝⁶ : 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
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
⊢ Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id

Tactic:
by
    have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
    exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

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✝⁶ : 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
tfae_1_to_3 : (Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_2_to_3 : (Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id) → ∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e
tfae_3_to_1 : (∃ e, f = ↑e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ ↑e) → Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id
e : N ≃ₗ[R] M × P
e₁ : f = ↑e.symm ∘ₗ inl R M P
e₂ : g = snd R M P ∘ₗ ↑e
⊢ Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id

Tactic:
by
    have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
    exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩

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✝⁶ : 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
⊢ [Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Surjective ⇑g ∧ ∃ 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
  | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩
  tfae_have 2 → 3
  | ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩
  tfae_have 3 → 1
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
    exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
  tfae_have 3 → 2
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
    exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
  tfae_finish

Goal state after:
Module: Mathlib.Order.RelSeries

Goal state before:
pp: case pos
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.natAdd p.length 0) = p.toFun i.succ

pp: case neg
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : ¬i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd (q.length + 1) ⟨↑i + 1, ⋯⟩) = p.toFun i.succ

Tactic:
· rw [Fin.addCases_right, h, ← last, connect, head]

Goal state after:
case neg
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
p q : RelSeries r
connect : p.last = q.head
i : Fin p.length
h : ¬i.succ = Fin.last p.length
⊢ Fin.addCases (p.toFun ∘ Fin.castSucc) q.toFun (Fin.castAdd (q.length + 1) ⟨↑i + 1, ⋯⟩) = p.toFun i.succ
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case inr.inl.mpr
α : Type u_1
inst✝ : Preorder α
n : ℕ
h✝¹ : Nonempty α
h✝ : FiniteDimensionalOrder α
⊢ (∃ l, l.length = n) → n ≤ (LTSeries.longestOf α).length

Tactic:
exact fun ⟨l, hl⟩ ↦ hl ▸ l.longestOf_is_longest

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
⊢ ⨆ p, ↑p.length < ↑↑0 ↔ ∀ (l : LTSeries α), l.length < 0

pp: case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1

Tactic:
· rw [ENat.natCast_zero, ← bot_eq_zero, WithBot.lt_coe_bot]
    simp

Goal state after:
case succ
α : Type u_1
inst✝ : Preorder α
n : ℕ
⊢ ⨆ p, ↑p.length < ↑↑(n + 1) ↔ ∀ (l : LTSeries α), l.length < n + 1
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
p : LTSeries (WithTop α)
hlast : RelSeries.last p = ↑x
p' : LTSeries α := { length := p.length, toFun := fun i ↦ (p.toFun i).untop ⋯, step := ⋯ }
hlast' : RelSeries.last p' = x
this : ↑p'.length ≤ height (RelSeries.last p')
⊢ ↑p.length ≤ height x

Tactic:
rw [hlast'] at this
      simpa [p'] using this

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

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 + a * a∗ ≤ a∗

Tactic:
add_le_iff

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a * a∗ ≤ a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 + a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗

Tactic:
add_le_iff

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a * a∗ ≤ a∗
this : 1 ≤ 1 + a * a∗ ∧ a * (1 + a * a∗) ≤ 1 + a * a∗
⊢ a∗ ≤ 1 + a * a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 + a∗ * a ≤ a∗

Tactic:
add_le_iff

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
⊢ 1 ≤ a∗ ∧ a∗ * a ≤ a∗
Module: Mathlib.Algebra.Order.Kleene

Goal state before:
pp: α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 + (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a

Tactic:
add_le_iff

Goal state after:
α : Type u_1
inst✝ : KleeneAlgebra α
a : α
h : 1 + a∗ * a ≤ a∗
this : 1 ≤ 1 + a∗ * a ∧ (1 + a∗ * a) * a ≤ 1 + a∗ * a
⊢ a∗ ≤ 1 + a∗ * a