mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case H.inr
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
⊢ ∏ x ∈ s, f x = 1

Tactic:
have : {x, g x hx} ⊆ s := by simp [insert_subset_iff, hx, g_mem]

Goal state after:
case H.inr
ι : Type u_1
M : Type u_4
s✝ : Finset ι
inst✝ : CommMonoid M
f : ι → M
s : Finset ι
ih :
  ∀ t ⊂ s,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ s → ι
hg₁ : ∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s
hg₄ : ∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a
x : ι
hx : x ∈ s
this : {x, g x hx} ⊆ s
⊢ ∏ x ∈ s, f x = 1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg
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
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
⊢ x ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}

Tactic:
refine hpwo.wellFoundedOn.induction ⟨hx₁, hx₂⟩ fun y ⟨hy₁, hy₂⟩ ih => ?_

Goal state after:
case neg
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
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
y : M
x✝ : y ∈ {x | x ∈ P ∧ x ≠ 1}
ih : ∀ z ∈ {x | x ∈ P ∧ x ≠ 1}, z ≤ y ∧ ¬y ≤ z → z ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
hy₁ : y ∈ P
hy₂ : y ≠ 1
⊢ y ∈ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x}
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ⁅p, q⁆ ∈ ↑N

Tactic:
rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]

Goal state after:
case refine_1
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
hcomm : IsMulCommutative (G ⧸ N)
p q : G
⊢ ↑(p * q * p⁻¹ * q⁻¹) = 1
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : ↑c * k x = ↑c * k y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
let ⟨d, hd⟩ := k.surjective c

Goal state after:
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
T : Submonoid P
Q : Type u_4
inst✝ : CommMonoid Q
k : P ≃* M
H : Submonoid.map k.toMonoidHom T = S
H' : comap k.toMonoidHom S = T
x y : P
c : ↥S
hc : ↑c * k x = ↑c * k y
d : P
hd : k d = ↑c
⊢ ∃ c, ↑c * x = ↑c * y
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
inst✝ : IsCancelMul M
n : N
ms : M × ↥S
eq : n * f ↑ms.2 = f ms.1
⊢ IsRightRegular n

Tactic:
exact (eq ▸ f.map_isRegular (isCancelMul_iff_forall_isRegular.mp ‹_› ms.1)).2.of_mul

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case zero
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)
⊢ x 0 < y 0

pp: case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 < y 0
n✝ : ℕ
hx : ∀ (k : ℕ), k < n✝ + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n✝ + 1 → f (y k) ≤ y (k + 1)
⊢ x (n✝ + 1) < y (n✝ + 1)

Tactic:
exacts [h₀, hf.seq_pos_lt_seq_of_lt_of_le (Nat.zero_lt_succ _) h₀.le hx hy]

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

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ v₁ < v₂ ∨ v₂ ≤ v₁

Tactic:
Classical.or_iff_not_imp_right

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r v₁ v₂ : α
h₁ : r ≤ v₁
h₂ : r ≤ v₂
⊢ ¬v₂ ≤ v₁ → v₁ < v₂
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
⊢ ¬BddAbove (Set.range f)

Tactic:
by
  rintro ⟨m, hm⟩
  have hm' : ∀ a, f a ≤ m := fun a ↦ hm <| Set.mem_range_self _
  obtain ⟨a₀⟩ := ‹Nonempty α›
  suffices ∀ b, f a₀ ≤ b → ∃ a, b < f a by
    obtain ⟨a, ha⟩ : ∃ a, m < f a := this m (hm' a₀)
    exact ha.not_ge (hm' a)
  have h : ∀ a, ∃ a', f a < f a' := fun a ↦ (exists_gt a).imp (fun a' h ↦ hf h)
  apply Succ.rec
  · exact h a₀
  rintro b _ ⟨a, hba⟩
  exact (h a).imp (fun a' ↦ (succ_le_of_lt hba).trans_lt)

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

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
⊢ Injective fun x ↦ n + x

Tactic:
add_comm n _

Goal state after:
n : ℕ∞
hn : n ≠ ⊤
⊢ Injective fun x ↦ x + n
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
push Not at h
    rw [prod_eq_one]
    exact fun i hi => if_neg (h i hi)

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

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ ∏ j, Function.update (fun j ↦ #(s j)) i 1 j = ∏ j ∈ univ.erase i, #(s j)

Tactic:
simp [prod_update_of_mem, erase_eq]

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ sSup s ∈ s

Tactic:
apply csSup_mem_of_not_isSuccLimit hs _ <| mt IsSuccLimit.isSuccPrelimit hlim

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
hs : s.Nonempty
⊢ BddAbove s
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (fun o ↦ o.toOption) ↑o = (↑o).toOption

Tactic:
dsimp; congr

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ x ≤ y ∨ y ≤ x

Tactic:
right

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
⊢ y ≤ x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ z ∨ f z ≤ f z

Tactic:
right

Goal state after:
case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ f z
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
right

Goal state after:
case image_self_subset_self.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
z : α
hz : z ∈ bot x f
hyz : f y ≤ z
⊢ f y ≤ f z
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
h' : f y ≤ z
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
right

Goal state after:
case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
h' : f y ≤ z
⊢ f y ≤ cSup c
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
h : ∀ (c : Set α), IsChain r c → ∃ ub, ∀ a ∈ c, r a ub
trans : ∀ {a b c : α}, r a b → r b c → r a c
this✝ : ∃ ub, ∀ a ∈ maxChain r, r a ub
ub : α
hub : ∀ a ∈ maxChain r, r a ub
a : α
ha : r ub a
this : IsChain r (insert a (maxChain r))
⊢ a ∈ maxChain r

Tactic:
by
      rw [maxChain_spec.right this (subset_insert _ _)]
      exact mem_insert _ _

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
r : α → α → Prop
c : Set α
hc : IsChain r c
⊢ ∃ M, IsMaxChain r M ∧ c ⊆ M

Tactic:
have H := zorn_subset_nonempty { s | c ⊆ s ∧ IsChain r s } ?_ c ⟨Subset.rfl, hc⟩
  · obtain ⟨M, hcM, hM⟩ := H
    exact ⟨M, ⟨hM.prop.2, fun d hd hMd ↦ hM.eq_of_subset ⟨hcM.trans hMd, hd⟩ hMd⟩, hcM⟩
  rintro cs hcs₀ hcs₁ ⟨s, hs⟩
  refine
    ⟨⋃₀cs, ⟨fun _ ha => Set.mem_sUnion_of_mem ((hcs₀ hs).left ha) hs, ?_⟩, fun _ =>
      Set.subset_sUnion_of_mem⟩
  rintro y ⟨sy, hsy, hysy⟩ z ⟨sz, hsz, hzsz⟩ hyz
  obtain rfl | hsseq := eq_or_ne sy sz
  · exact (hcs₀ hsy).right hysy hzsz hyz
  rcases hcs₁ hsy hsz hsseq with h | h
  · exact (hcs₀ hsz).right (h hysy) hzsz hyz
  · exact (hcs₀ hsy).right hysy (h hzsz) hyz

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc' : cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ ¬cSup c ≤ y

Tactic:
intro hc'

Goal state after:
case cSup_mem.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
hz : y ∈ c
hzy : ¬f y ≤ y
h : y ≤ y
hc'✝ : cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
hc' : cSup c ≤ y
⊢ False
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : z ≤ y
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z ∨ (fun x1 x2 ↦ x1 ≤ x2) z y

Tactic:
right

Goal state after:
case inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : z ≤ y
⊢ (fun x1 x2 ↦ x1 ≤ x2) z y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
have hs : (g '' (f '' s)ᶜ)ᶜ = s := F.map_lfp

Goal state after:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
have g'g : LeftInverse g' g := leftInverse_invFun hg

Goal state after:
case inr
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
f : α → β
g : α →𝒄 β
h : f = ⇑g
⊢ ∀ (c : Chain α), (g.copy f h).toFun (ωSup c) = ωSup (c.map (g.copy f h))

Tactic:
by rw [OrderHom.copy_eq]; exact g.map_ωSup'

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

Goal state before:
pp: case refine_1
α β : Type u
a b : Cardinal.{u}
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

Tactic:
refine inductionOn₂ a b fun _ _ ↦ ?_

Goal state after:
case refine_1
α β : Type u
a b : Cardinal.{u}
x✝¹ x✝ : Type u
⊢ lift.{v, u} #x✝¹ ≤ lift.{v, u} #x✝ ↔ #x✝¹ ≤ #x✝
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{v}
⊢ toNat (lift.{u, v} c) = toNat c

Tactic:
simp only [← toNat_toENat, toENat_lift]

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

Goal state before:
pp: s : Set Cardinal.{u_1}
⊢ sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rcases s.eq_empty_or_nonempty with rfl | hne
    · exact Or.inl rfl
    · exact Or.inr ⟨sInf s, csInf_mem hne, h⟩
  · rcases h with rfl | ⟨a, ha, rfl⟩
    · exact Cardinal.sInf_empty
    · exact eq_bot_iff.2 (csInf_le' ha)

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

Goal state before:
pp: ⊢ 1 < ℵ₀

Tactic:
simpa using natCast_lt_aleph0 (n := 1)

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

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
right

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
right

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u_1
s : Set α
n : ℕ
⊢ (∃ t, ↑t = s ∧ t.card = n) → #↑s = ↑n

Tactic:
rintro ⟨t, rfl, rfl⟩

Goal state after:
case mpr
α : Type u_1
t : Finset α
⊢ #↑↑t = ↑t.card
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ lift.{v, u} #↑(⇑f ⁻¹' s) = lift.{u, v} #↑s

Tactic:
apply mk_preimage_of_injective_of_subset_range_lift _ _ f.injective

Goal state after:
α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ s ⊆ range ⇑f
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ f = g ∘ₛₗ ↑e₁₂.symm ↔ f ∘ₛₗ ↑e₁₂ = g

Tactic:
constructor <;> intro H <;> ext

Goal state after:
case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f = g ∘ₛₗ ↑e₁₂.symm
x✝ : M₁
⊢ (f ∘ₛₗ ↑e₁₂) x✝ = g x✝

case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ ↑e₁₂ = g
x✝ : M₂
⊢ f x✝ = (g ∘ₛₗ ↑e₁₂.symm) x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ f = g ∘ₛₗ ↑e₁₂.symm ↔ f ∘ₛₗ ↑e₁₂ = g

Tactic:
by
  constructor <;> intro H <;> ext
  · simp [H]
  · simp [← H]

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

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
⊢ g ∘ₛₗ ↑e₁₂.symm = f ↔ g = f ∘ₛₗ ↑e₁₂

Tactic:
constructor <;> intro H <;> ext

Goal state after:
case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g ∘ₛₗ ↑e₁₂.symm = f
x✝ : M₁
⊢ g x✝ = (f ∘ₛₗ ↑e₁₂) x✝

case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : g = f ∘ₛₗ ↑e₁₂
x✝ : M₂
⊢ (g ∘ₛₗ ↑e₁₂.symm) x✝ = f x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
⊢ f = ↑e₁₂.symm ∘ₛₗ g ↔ ↑e₁₂ ∘ₛₗ f = g

Tactic:
constructor <;> intro H <;> ext

Goal state after:
case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : f = ↑e₁₂.symm ∘ₛₗ g
x✝ : M₃
⊢ (↑e₁₂ ∘ₛₗ f) x✝ = g x✝

case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
H : ↑e₁₂ ∘ₛₗ f = g
x✝ : M₃
⊢ f x✝ = (↑e₁₂.symm ∘ₛₗ g) x✝
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₃₁ : R₃ →+* R₁
σ₃₂ : R₃ →+* R₂
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂
f : M₃ →ₛₗ[σ₃₁] M₁
g : M₃ →ₛₗ[σ₃₂] M₂
⊢ f = ↑e₁₂.symm ∘ₛₗ g ↔ ↑e₁₂ ∘ₛₗ f = g

Tactic:
by
  constructor <;> intro H <;> ext
  · simp [H]
  · simp [← H]

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

Goal state before:
pp: M : Type u_8
M₂ : Type u_10
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₂
R : Type u_14
S : Type u_15
inst✝⁷ : Semiring S
inst✝⁶ : SMul R M
inst✝⁵ : Module S M
inst✝⁴ : SMul R M₂
inst✝³ : Module S M₂
inst✝² : SMul R S
inst✝¹ : CompatibleSMul M M₂ R S
inst✝ : IsScalarTower R S M₂
f : M →ₗ[S] M₂
hf : Injective ⇑f
r : R
s : S
x✝ : M
⊢ f ((r • s) • x✝) = f (r • s • x✝)

Tactic:
by rw [f.map_smul_of_tower r, map_smul, map_smul, smul_assoc]

Goal state after: