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

Goal state before:
pp: case inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
⊢ n = sInf {m | p m}

Tactic:
obtain hnp | hnp := hn.eq_or_lt

Goal state after:
case inl.inl
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n = sInf {m | p m}
⊢ n = sInf {m | p m}

case inl.inr
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m | p m}
h : {m | p (m + n)} = ∅
hnp : n < sInf {m | p m}
⊢ n = sInf {m | p m}
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b : ℕ
⊢ Ico a.succ b = (Ico a b).erase a

Tactic:
by
  ext x
  simp_rw [mem_erase, mem_Ico]
  lia

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mp
α : Type u_2
r : α → α → Prop
inst✝ : IsStrictOrder α r
s : Set α
⊢ Nonempty ((fun x1 x2 ↦ x1 > x2) ↪r fun a b ↦ r a b ∧ a ∈ s ∧ b ∈ s) → ∃ x, ∀ (n : ℕ), x n ∈ s

Tactic:
rintro ⟨⟨f, hf⟩⟩
    have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2
    refine ⟨⟨f, ?_⟩, H⟩
    simpa only [H, and_true] using @hf

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_3
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
x✝ : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
this : WellQuasiOrderedLE α
⊢ WellFounded fun a b ↦ r a b ∧ ¬r b a

Tactic:
exact wellFounded_lt

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
⊢ IsAntichain (fun x1 x2 ↦ x1 ≤ x2) (Set.range (f ∘ ⇑g))

pp: case inr.refine_2
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
⊢ (Set.range (f ∘ ⇑g)).Infinite

Tactic:
· rintro _ ⟨m, rfl⟩ _ ⟨n, rfl⟩ _ hf
      obtain h | rfl | h := lt_trichotomy m n
      · exact hc _ _ (g.strictMono h) hf
      · contradiction
      · exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : Preorder α
x✝ : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f (g m) > f (g n)
hc : ∀ (m n : ℕ), m < n → ¬f m ≤ f n
⊢ (Set.range (f ∘ ⇑g)).Infinite
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b

Tactic:
ext
  simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f (g m) i) (f (g n) i)
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)

Tactic:
obtain ⟨g', hg'⟩ := ih (f ∘ g) (hf <| g ·)

Goal state after:
case refine_2
ι : Type u_1
α : ι → Type u_6
inst✝¹ : Finite ι
r : (i : ι) → α i → α i → Prop
inst✝ : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this✝ : Fintype ι
this : IsPreorder ((i : ι) → α i) fun a b ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) → ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ ⇑g) a i) ((f ∘ ⇑g) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f (g m) i) (f (g n) i)
g' : ℕ ↪o ℕ
hg' : ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i (((f ∘ ⇑g) ∘ ⇑g') a i) (((f ∘ ⇑g) ∘ ⇑g') b i)
⊢ ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ ⇑g) a i_1) ((f ∘ ⇑g) b i_1)
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ s ^ n * ↑(closure s) = ↑(closure s)

Tactic:
pow_mul_subgroupClosure hs

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
n : ℕ
⊢ ↑(closure s) = ↑(closure s)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute ((f * g) x) ((f * g) y)

Tactic:
apply Commute.mul_left

Goal state after:
case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) ((f * g) y)

case hbc
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) ((f * g) y)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
hu : s' ⊆ s
hf : ∀ c ∈ s, c ∉ s' → f c = 1
⊢ ∏ x ∈ s', f x = f a * f b

Tactic:
exact Finset.prod_pair hn

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
this : Fintype ι
x : (i : ι) → M i
hx : x ∈ pi Set.univ P
⊢ x ∈ ⨆ i, map (MonoidHom.mulSingle M i) (P i)

Tactic:
rw [← Finset.noncommProd_mulSingle x]

Goal state after:
ι : Type u_3
inst✝² : Finite ι
M : ι → Type u_4
inst✝¹ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
inst✝ : DecidableEq ι
this : Fintype ι
x : (i : ι) → M i
hx : x ∈ pi Set.univ P
⊢ Finset.univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯ ∈ ⨆ i, map (MonoidHom.mulSingle M i) (P i)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ FG ↥(Subgroup.closure ↑s)

Tactic:
by
  refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩
  rw [Finset.coe_preimage, ← Subgroup.coe_subtype, Subgroup.closure_preimage_eq_top]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
⊢ P.FG

Tactic:
have hpwo := Set.isPWO_of_wellQuasiOrderedLE { x | x ∈ P ∧ x ≠ 1 }
  rw [fg_iff]
  refine ⟨_, ?_, (setOfPred_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOfPred_minimal_subset _))⟩
  ext x
  constructor
  · intro hx
    rw [← P.closure_eq]
    exact closure_mono ((setOfPred_minimal_subset _).trans fun _ => And.left) hx
  · intro hx₁
    by_cases hx₂ : x = 1
    · simp [hx₂]
    refine hpwo.wellFoundedOn.induction ⟨hx₁, hx₂⟩ fun y ⟨hy₁, hy₂⟩ ih => ?_
    simp only [Set.mem_ofPred_eq, and_imp] at ih
    by_cases hy₃ : Minimal (· ∈ { x | x ∈ P ∧ x ≠ 1 }) y
    · exact mem_closure_of_mem hy₃
    rcases exists_lt_of_not_minimal ⟨hy₁, hy₂⟩ hy₃ with ⟨z, hz₁, hz₂, hz₃⟩
    rcases exists_mul_of_le hz₁.le with ⟨y, rfl⟩
    apply mul_mem
    · exact ih _ hz₂ hz₃ hz₁.le hz₁.not_ge
    apply ih
    · exact hP _ hz₂ _ hy₁
    · exact (one_lt_of_lt_mul_right hz₁).ne.symm
    · exact le_mul_self
    · rw [mul_le_iff_le_one_left']
      exact (one_lt_of_ne_one hz₃).not_ge

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
⊢ ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
    rw [← map_commutatorElement]
    exact mem_map_of_mem _ (commutator_mem_commutator hp hq)

Goal state after:
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ center G

Tactic:
rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
    Subgroup.commutator_eq_bot_iff_le_centralizer]
  suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
    refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
  rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
  exact Set.centralizer_subset (Subgroup.commutator_mono le_top le_top)

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
S : Submonoid M
f : M → G
hf : Injective f
surj : ∀ (g : G), ∃ x, ∃ y ∈ S, g = f x / f y
x✝ y✝ : M
eq : f x✝ = f y✝
⊢ ∃ c, ↑c * x✝ = ↑c * y✝

Tactic:
simp [hf eq]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (n₁ * (f ↑ms₁.2 * f ↑ms₂.2)) = f m * (n₂ * (f ↑ms₁.2 * f ↑ms₂.2))
⊢ n₁ * (f ↑ms₁.2 * f ↑ms₂.2) = n₂ * (f ↑ms₁.2 * f ↑ms₂.2)

Tactic:
← mul_assoc n₁,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (n₁ * f ↑ms₁.2 * f ↑ms₂.2) = f m * (n₂ * (f ↑ms₁.2 * f ↑ms₂.2))
⊢ n₁ * f ↑ms₁.2 * f ↑ms₂.2 = n₂ * (f ↑ms₁.2 * f ↑ms₂.2)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

pp: case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
· simpa [ha.succ_eq] using le_of_eq

Goal state after:
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ a < b ↔ ∃ c < b, a < c

Tactic:
by
  rw [← not_iff_not]
  simp [h.le_iff_forall_le]

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

Goal state before:
pp: m n a b : ℕ
h : a ≤ b
⊢ Order.succ^[b - a] a = b

Tactic:
rw [succ_eq_succ, Nat.succ_iterate, add_tsub_cancel_of_le h]

Goal state after:
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
⊢ ∀ (a b : SuccOrder α), a = b

Tactic:
by
    intro h₀ h₁
    ext a
    by_cases ha : IsMax a
    · exact (@IsMax.succ_eq _ _ h₀ _ ha).trans ha.succ_eq.symm
    · exact @CovBy.succ_eq _ _ h₀ _ _ (covBy_succ_of_not_isMax ha)

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
inst✝¹ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
f g f' g' : (i : ι) → π i
inst✝ : (i : ι) → Preorder (π i)
hf : ∀ x ∈ s, f x ≤ f' x
hg : ∀ x ∉ s, g x ≤ g' x
x : ι
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

Tactic:
by by_cases hx : x ∈ s <;> simp [*]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
u : Finset (α ⊕ β)
⊢ u.toRight = ∅ ↔ u ⊆ map Function.Embedding.inl univ

Tactic:
simp [subset_map_inl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Fintype α
t : Finset β
hαt : Fintype.card α = #t
s : Set α
f : α → β
hfst : MapsTo f s ↑t
hfs : InjOn f s
⊢ ∃ g, ∀ i ∈ s, ↑(g i) = f i

Tactic:
by
  classical
    let s' : Finset α := s.toFinset
    have hfst' : s'.image f ⊆ t := by simpa [s', ← Finset.coe_subset] using! hfst
    have hfs' : Set.InjOn f s' := by simpa [s'] using! hfs
    obtain ⟨g, hg⟩ := Finset.exists_equiv_extend_of_card_eq hαt hfst' hfs'
    refine ⟨g, fun i hi => ?_⟩
    apply hg
    simpa [s'] using! hi

Goal state after:
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
s : Sym α (n✝ + 1)
⊢ ∀ (b : Sym α (n✝ + 1)), s = b

Tactic:
s'

Goal state after:
case succ
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
inst✝ : Subsingleton α
n✝ : ℕ
s s' : Sym α (n✝ + 1)
⊢ s = s'
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Tactic:
toList_reverse

Goal state after:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.toList.reverse.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
v₁ : Vector α n
v₂ : Vector β n
f : α → β → γ
i : Fin n
⊢ (map₂ f v₁ v₂).get i = f (v₁.get i) (v₂.get i)

Tactic:
induction v₁, v₂ using inductionOn₂ with
  | nil =>
    exact Fin.elim0 i
  | cons ih =>
    rw [map₂_cons]
    cases i using Fin.cases
    · simp only [get_zero, head_cons]
    · simp only [get_cons_succ, ih]

Goal state after:
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
⊢ ∀ (a b c : α ⊕ β), Lex r s a b → Lex r s b c → Lex r s a c

Tactic:
rintro _ _ _ (⟨hab⟩ | ⟨hab⟩) (⟨hbc⟩ | ⟨hbc⟩)

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝¹ : α
hab : r a₁✝ a₂✝¹
a₂✝ : α
hbc : r a₂✝¹ a₂✝
⊢ Lex r s (inl a₁✝) (inl a₂✝)

case inl.sep
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
b✝ : β
⊢ Lex r s (inl a₁✝) (inr b✝)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
b₁✝ b₂✝¹ : β
hab : s b₁✝ b₂✝¹
b₂✝ : β
hbc : s b₂✝¹ b₂✝
⊢ Lex r s (inr b₁✝) (inr b₂✝)

case sep.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a✝ : α
b✝ b₂✝ : β
hbc : s b✝ b₂✝
⊢ Lex r s (inl a✝) (inr b₂✝)
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
a✝ b✝ : Lex (α × β)
a b : α × β
⊢ { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex a) ≤
      { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex b) ↔
    toLex a ≤ toLex b

Tactic:
by
    simpa [Prod.Lex.toLex_le_toLex] using le_iff_lt_or_eq

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
⊢ ScottContinuousOn D (g ∘ f)

Tactic:
intro d hd₁ hd₂ hd₃ a ha

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : β → γ
D' : Set (Set β)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hD' : MapsTo (fun x ↦ f '' x) D D'
hg : ScottContinuousOn D' g
hf : ScottContinuousOn D f
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
ha : IsLUB d a
⊢ IsLUB (g ∘ f '' d) ((g ∘ f) a)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
⊢ ScottContinuousOn D Prod.fst

Tactic:
intro d hd₁ hd₂ hd₃ a ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB d a
⊢ IsLUB (Prod.fst '' d) a.1
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
⊢ ScottContinuousOn D Prod.snd

Tactic:
intro d hd₁ hd₂ hd₃ a ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB d a
⊢ IsLUB (Prod.snd '' d) a.2
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: n : ℕ
⊢ lift.{u, v} ↑n = ↑n

Tactic:
by induction n <;> simp [*]

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

Goal state before:
pp: m : ℕ∞
⊢ 0 = ↑m ↔ m = 0

Tactic:
norm_cast; apply eq_comm

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

Goal state before:
pp: m : ℕ∞
⊢ 1 = ↑m ↔ m = 1

Tactic:
norm_cast; apply eq_comm

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c

Tactic:
exact not_isSuccLimit_of_lt_aleph0 h

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

Goal state before:
pp: α : Type u
x : α
⊢ 2 ≤ #α ↔ ∃ y, y ≠ x

Tactic:
by
  rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]

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

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
⊢ f 0 = 0

Tactic:
rw [← zero_smul R (0 : M), map_smulₛₗ]

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
F : Type u_14
inst✝¹⁰ : Semiring R
inst✝⁹ : Semiring S
inst✝⁸ : AddCommMonoid M
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M₃
inst✝⁴ : Module R M
inst✝³ : Module R M₂
inst✝² : Module S M₃
σ : R →+* S
inst✝¹ : FunLike F M M₃
inst✝ : SemilinearMapClass F σ M M₃
f : F
⊢ σ 0 • f 0 = 0
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).1 = ↑n

Tactic:
by induction n <;> simp [*]

Goal state after:
Module: Mathlib.Data.Nat.Cast.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).2 = ↑n

Tactic:
by induction n <;> simp [*]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
hH : map (fst M N) u ≤ s
hK : map (snd M N) u ≤ t
x1 : M
x2 : N
h : (x1, x2) ∈ u
⊢ (x1, x2) ∈ s.prod t

Tactic:
exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t → u ≤ s.prod t

Tactic:
rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ r • m = (algebraMap R A) r • m

Tactic:
← one_smul A m,

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
A : Type u_2
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
r : R
m : M
⊢ r • 1 • m = (algebraMap R A) r • 1 • m
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: F : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Monoid M
inst✝³ : Monoid N
f : F
x : M
inst✝² : FunLike F M N
inst✝¹ : MonoidHomClass F M N
inst✝ : IsLocalHom f
hfx : Irreducible (f x)
⊢ ∀ ⦃a b : M⦄, x = a * b → IsUnit a ∨ IsUnit b

Tactic:
rintro p q rfl; exact (hfx.isUnit_or_isUnit <| map_mul f p q).imp (.of_map f _) (.of_map f _)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∉ M₀⁰ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty

Tactic:
simp [mem_nonZeroDivisors_iff_left, Set.nonempty_def]

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e e₁ : A₁ ≃ₐ[R] A₂
e₂ : A₂ ≃ₐ[R] A₃
r : R
⊢ e₂.toFun (e₁.toFun ((algebraMap R A₁) r)) = (algebraMap R A₃) r

Tactic:
rw [e₁.commutes', e₂.commutes']

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
h₁ : f ∘ₛₗ 0 = 0
⊢ f.ker = ⊥

Tactic:
rw [← Submodule.range_subtype (ker f),
    ← h 0 (ker f).subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
h₁ : f ∘ₛₗ 0 = 0
⊢ range 0 = ⊥
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
h : ∀ (u v : ↥f.ker →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = v
⊢ f.ker = ⊥

Tactic:
by
  have h₁ : f.comp (0 : ker f →ₗ[R] M) = 0 := comp_zero _
  rw [← Submodule.range_subtype (ker f),
    ← h 0 (ker f).subtype (Eq.trans h₁ (comp_ker_subtype f).symm)]
  exact range_zero

Goal state after: