mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m

Tactic:
rw [WithBot.coe_lt_coe, Nat.cast_add, natCast_one, ENat.lt_add_one_iff (natCast_ne_top _),
      ← WithBot.coe_le_coe, WithBot.coe_natCast]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f (pred a) < f a

Tactic:
by simpa using hf

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ ∀ (a : α), ¬IsMin a → a ∈ Set.univ → pred a ∈ Set.univ → f a < f (pred a)

Tactic:
by simpa using hf

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
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩

Tactic:
· apply Function.hfunext <;> simp +contextual [Subtype.heq_iff_coe_eq]

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : a = x then b x h else 1) = b a ⋯

Tactic:
rw [Finset.prod_eq_single a, dif_pos rfl]
    · intro _ _ h
      rw [dif_neg]
      exact h.symm
    · simp [h]

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: case e_toSeqRight
F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
toLawfulFunctor✝¹ : LawfulFunctor F
seqLeft_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq1 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq1 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝¹ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝¹ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
toLawfulFunctor✝ : LawfulFunctor F
seqLeft_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x <* y = const β <$> x <*> y
seqRight_eq2 : ∀ {α β : Type u} (x : F α) (y : F β), x *> y = const α id <$> x <*> y
pure_seq2 : ∀ {α β : Type u} (g : α → β) (x : F α), pure g <*> x = g <$> x
seq_pure✝ : ∀ {α β : Type u} (g : F (α → β)) (x : α), g <*> pure x = (fun h ↦ h x) <$> g
seq_assoc✝ : ∀ {α β γ : Type u} (x : F α) (g : F (α → β)) (h : F (β → γ)), h <*> (g <*> x) = comp <$> h <*> g <*> x
α β : Type u
x : F α
y : Unit → F β
⊢ sr1 x y = sr2 x y

Tactic:
exact (seqRight_eq1 _ (y Unit.unit)).trans (seqRight_eq2 _ (y Unit.unit)).symm

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mpr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
⊢ (∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤) → ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
rintro ⟨S, hSc, hps, hS⟩

Goal state after:
case mpr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: case inr.inl
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : ¬r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inl ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inl ⟨b, hb⟩)

pp: case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)

Tactic:
· simpa using fun h ↦ hb <| trans ha h

Goal state after:
case inr.inr
α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
a : α
ha : r x a
b : α
hb : r x b
⊢ r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨a, ha⟩))
      (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) (Sum.inr ⟨b, hb⟩)) ↔
    Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) (Sum.inr ⟨a, ha⟩) (Sum.inr ⟨b, hb⟩)
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
⊢ ∀ {a b : Lex ((α ⊕ₗ β) × γ)},
    (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.sumProdDistrib α β γ).trans ((toLex.sumCongr toLex).trans toLex))))
          a ≤
        (ofLex.trans
            ((ofLex.prodCongr (Equiv.refl γ)).trans
              ((Equiv.sumProdDistrib α β γ).trans ((toLex.sumCongr toLex).trans toLex))))
          b ↔
      a ≤ b

Tactic:
simp [Prod.Lex.le_iff]

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝¹ : Type u_1
α✝ : Type u_2
β✝ : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
δ : Type u_7
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
ea : α ≃o β
eb : γ ≃o δ
⊢ ∀ {a b : Lex (α × γ)},
    (ofLex.trans (((↑ea).prodCongr ↑eb).trans toLex)) a ≤ (ofLex.trans (((↑ea).prodCongr ↑eb).trans toLex)) b ↔ a ≤ b

Tactic:
simp [Prod.Lex.le_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
a : α
⊢ (∀ ⦃b : α⦄, a ≤ b → a ∈ s → b ∈ s) ↔ ∀ ⦃b : α⦄, a < b → a ∈ s → b ∈ s

Tactic:
by simp [le_iff_eq_or_lt, or_imp, forall_and]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsLUB (Set.range ⇑c) (ωSup c)

Tactic:
constructor
  · simp only [upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
      Set.mem_ofPred_eq]
    exact fun a ↦ le_ωSup c a
  · simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index,
      forall_apply_eq_imp_iff, Set.mem_ofPred_eq]
    exact fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
rcases c.eq_empty_or_nonempty with (rfl | ⟨y, hy⟩)
    · exact ⟨x, ⟨hxs, le_rfl⟩, fun z => False.elim⟩
    · rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩
      exact ⟨z, ⟨hzs, (hcs hy).2.trans <| hz _ hy⟩, hz⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ ωScottContinuous ⇑f ↔ ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

Tactic:
rw [ωScottContinuous_iff_monotone_map_ωSup]

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ (∃ (hf : Monotone ⇑f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := ⇑f, monotone' := hf })) ↔
    ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case pos
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ∃ a, some a ∈ c
h : a ∈ some (Classical.choose h_1)
⊢ some a ∈ c

pp: case neg
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ¬∃ a, some a ∈ c
h : a ∈ none
⊢ some a ∈ c

Tactic:
· have h' := Classical.choose_spec h_1
    rw [← eq_some_iff] at h
    rw [← h]
    exact h'

Goal state after:
case neg
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ¬∃ a, some a ∈ c
h : a ∈ none
⊢ some a ∈ c
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x y : Cardinal.{u}
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
by
    wlog hle : x ≤ y; · rw [add_comm, this y x (le_of_not_ge hle), add_comm]
    cases lt_or_ge y ℵ₀ with
    | inl hy =>
      lift x to ℕ using hle.trans_lt hy; lift y to ℕ using hy
      simp only [← Nat.cast_add, toENatAux_nat]
    | inr hy =>
      simp only [toENatAux_eq_top hy, add_top]
      exact toENatAux_eq_top <| le_add_left hy

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

Goal state before:
pp: c c' : Cardinal.{u}
hc : c ≤ ℵ₀
⊢ toENat c ≤ toENat c' ↔ c ≤ c'

Tactic:
by
  lift c to ℕ∞ using hc; simp_rw [toENat_ofENat, enat_gc _]

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

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

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hne

Goal state after:
case refine_1.inl
h : sInf ∅ = 0
⊢ ∅ = ∅ ∨ ∃ a ∈ ∅, a = 0

case refine_1.inr
s : Set Cardinal.{u_1}
h : sInf s = 0
hne : s.Nonempty
⊢ s = ∅ ∨ ∃ a ∈ s, a = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
let h := (@mul_lt_aleph0_iff a b).not
  rwa [not_lt, not_or, not_or, not_and_or, not_lt, not_lt] at h

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

Goal state before:
pp: α : Type u
⊢ Infinite α ↔ ℵ₀ ≤ #α

Tactic:
rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ compHom α (MonoidHom.inr M N) = hN

pp: case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝

Tactic:
· ext n a; (conv_rhs => rw [← hM.one_smul (SMul.smul n a)]); rfl

Goal state after:
case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
ι : Sort u_9
f : M →ₛₗ[σ₁₂] M₂
p : ι → Submodule R₂ M₂
⊢ comap f (⨅ i, p i) = ⨅ i, comap f (p i)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ p ≤ comap f (map (a • f) p)

Tactic:
← comap_smul f _ a h,

Goal state after:
K : Type u_9
V : Type u_10
V₂ : Type u_11
inst✝⁴ : Semifield K
inst✝³ : AddCommMonoid V
inst✝² : Module K V
inst✝¹ : AddCommMonoid V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
p : Submodule K V
a : K
h : a ≠ 0
⊢ p ≤ comap (a • f) (map (a • f) p)
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M
inst✝² : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝¹ : RingHomInvPair τ₁₂ τ₂₁
inst✝ : RingHomInvPair τ₂₁ τ₁₂
p : Submodule R M
e : M ≃ₛₗ[τ₁₂] M₂
x : M₂
⊢ x ∈ map (↑e) p ↔ e.symm x ∈ p

Tactic:
rw [Submodule.mem_map]; constructor
  · rintro ⟨y, hy, hx⟩
    simp [← hx, hy]
  · intro hx
    exact ⟨e.symm x, hx, by simp⟩

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

Goal state before:
pp: case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
⊢ (∃ (hx'' : x₃ ∈ ⨆ i, S i), C x₃ hx'') →
    (∃ (hx'' : y ∈ ⨆ i, S i), C y hx'') → ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''

Tactic:
rintro ⟨_, Cx⟩ ⟨_, Cy⟩

Goal state after:
case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
w✝¹ : x₃ ∈ ⨆ i, S i
Cx : C x₃ w✝¹
w✝ : y ∈ ⨆ i, S i
Cy : C y w✝
⊢ ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
⊢ ↑(⊥.prod ⊥) = ↑⊥

Tactic:
simp [coe_prod]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : NonUnitalNonAssocSemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ srange f = map f ⊤

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit (↑h.unit⁻¹ m) = ↑h.unit m'

Tactic:
rw [H]

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit (↑h.unit⁻¹ (x • m')) = ↑h.unit m'
Module: Mathlib.Algebra.Algebra.Basic

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit (↑h.unit⁻¹ (x • m')) = ↑h.unit m'

Tactic:
simpa using Module.End.isUnit_apply_inv_apply_of_isUnit h (x • m')

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
⊢ f.rangeS = Subsemiring.map f ⊤

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit m' = ↑h.unit (↑h.unit⁻¹ m)

Tactic:
rw [H]

Goal state after:
R : Type u
S : Type v
M : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Module S M
inst✝² : SMulCommClass S R M
inst✝¹ : SMul R S
inst✝ : IsScalarTower R S M
x : R
h : IsUnit ((algebraMap R (End S M)) x)
m m' : M
H : m = x • m'
⊢ ↑h.unit m' = ↑h.unit (↑h.unit⁻¹ (x • m'))
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
⊢ f.range = Subring.map f ⊤

Tactic:
by
  ext
  simp

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

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a b : M
hab : a ∣ b
hba : b ∣ a
⊢ a ~ᵤ b

Tactic:
rcases hab with ⟨c, rfl⟩
  rcases hba with ⟨d, a_eq⟩
  by_cases ha0 : a = 0
  · simp_all
  have hac0 : a * c ≠ 0 := by
    intro con
    rw [con, zero_mul] at a_eq
    apply ha0 a_eq
  have : a * (c * d) = a * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
  have hcd : c * d = 1 := mul_left_cancel₀ ha0 this
  have : a * c * (d * c) = a * c * 1 := by rw [← mul_assoc, ← a_eq, mul_one]
  have hdc : d * c = 1 := mul_left_cancel₀ hac0 this
  exact ⟨⟨c, d, hcd, hdc⟩, rfl⟩

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ comap f (map f s) = s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
apply le_antisymm
  · intro x hx
    rw [mem_comap, mem_map] at hx
    obtain ⟨y, hy, hxy⟩ := hx
    replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
    rw [← closure_eq s, ← closure_union, ← add_sub_cancel y x]
    exact Subring.add_mem _ (subset_closure <| Or.inl hy) (subset_closure <| Or.inr hxy)
  · rw [← map_le_iff_le_comap, map_sup, f.map_closure]
    apply le_of_eq
    rw [sup_eq_left, closure_le]
    exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)

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₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
⊢ f.range = map f ⊤

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ (↑e).comp ↑e.symm = AlgHom.id R A₂

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A₁
inst✝² : Semiring A₂
inst✝¹ : Algebra R A₁
inst✝ : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
⊢ (↑e.symm).comp ↑e = AlgHom.id R A₁

Tactic:
by
  ext
  simp

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₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
e₃ : A₃ ≃ₐ[R] A₃'
f : A₁ →ₐ[R] A₂
g : A₂ →ₐ[R] A₃
⊢ (e₁.arrowCongr e₃) (g.comp f) = ((e₂.arrowCongr e₃) g).comp ((e₁.arrowCongr e₂) f)

Tactic:
by
  ext
  simp

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

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ i.range
⊢ i ∘ₗ f.codRestrictOfInjective i hi hf = f

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
c : ClosureOperator α
⊢ c = ofPred (⇑c) c.IsClosed ⋯ ⋯ ⋯

Tactic:
by
  ext
  simp

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ (K ≠ ⊥ ∧ ∀ (b : A) (x : B), x ∈ K ∧ x ∉ b → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
← and_imp,

Goal state after:
A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ (K ≠ ⊥ ∧ ∀ (b : A) (x : B), (x ∈ K ∧ x ∉ b) ∧ b ≤ K → b = ⊥) ↔
    K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K ∧ g ∉ H ∧ g ∈ K → H = ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderBot A
K : A
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
simp_rw [IsAtom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderTop A
K : A
⊢ (K ≠ ⊤ ∧ ∀ (b : A) (x : B), x ∈ b ∧ x ∉ K → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

Tactic:
← and_imp,

Goal state after:
A : Type u_4
B : Type u_5
inst✝³ : PartialOrder A
inst✝² : SetLike A B
inst✝¹ : IsConcreteLE A B
inst✝ : OrderTop A
K : A
⊢ (K ≠ ⊤ ∧ ∀ (b : A) (x : B), (x ∈ b ∧ x ∉ K) ∧ K ≤ b → b = ⊤) ↔
    K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H ∧ g ∉ K ∧ g ∈ H → H = ⊤
Module: Mathlib.Order.SupClosed

Goal state before:
pp: ι : Sort u_1
F : Type u_2
α : Type u_3
β : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s t : Set α
a b : α
⊢ ∀ (x : Set α), SupClosed {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ x ∧ t.sup' ht id = a}

Tactic:
classical
    rintro s _ ⟨t, ht, hts, rfl⟩ _ ⟨u, hu, hus, rfl⟩
    refine ⟨_, ht.mono subset_union_left, ?_, sup'_union ht hu _⟩
    rw [coe_union]
    exact Set.union_subset hts hus

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ (supClosure ↑s).Finite

Tactic:
refine ({t ∈ s.powerset | t.Nonempty}.attach.image
    fun t ↦ t.1.sup' (mem_filter.1 t.2).2 id).finite_toSet.subset ?_

Goal state after:
α : Type u_3
inst✝ : SemilatticeSup α
s : Finset α
⊢ supClosure ↑s ⊆ ↑(Finset.image (fun t ↦ (↑t).sup' ⋯ id) {t ∈ s.powerset | t.Nonempty}.attach)
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
x✝ : a ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : a ≤ sSup S
hatom : IsAtom a
⊢ a ∈ S

Tactic:
obtain ⟨b, hbS, hba⟩ := (IsAtom.le_sSup hatom).mp hale

Goal state after:
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
x✝ : a ∈ {a | a ≤ sSup S ∧ IsAtom a}
hale : a ≤ sSup S
hatom : IsAtom a
b : α
hbS : b ∈ S
hba : a ≤ b
⊢ a ∈ S
Module: Mathlib.Order.Atoms

Goal state before:
pp: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b c : α
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)
    · simp
    · rcases eq_bot_or_eq_top b with (rfl | rfl)
      · rcases eq_bot_or_eq_top c with (rfl | rfl) <;> simp
      · simp

Goal state after: