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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
β : Type u_4
γ : Type u_5
s✝ : Finset ι
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
f : (x : ι) → p x → M
g : (x : ι) → ¬p x → M
x : ↥({x ∈ s | ¬p x})
⊢ ¬p ↑x

Tactic:
by simpa using (mem_filter.mp x.2).2

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ (∏ x ∈ s, if x ∈ t then f x else g x) = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

Tactic:
prod_ite,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ (∏ x ∈ s with x ∈ t, f x) * ∏ x ∈ s with x ∉ t, g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n.succ
⊢ ∃ a s', s = a ::ₛ s'

Tactic:
obtain ⟨a, ha⟩ := exists_mem s
  classical exact ⟨a, s.erase a ha, (cons_erase ha).symm⟩

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

Goal state before:
pp: n : ℕ
α β : Type u_6
f : α → β
⊢ ∀ (x : Vector α n), Vector.traverse (pure ∘ f) x = pure (map f x)

Tactic:
by
  rintro ⟨x, rfl⟩
  simp!
  induction x <;> simp! [*, functor_norm]
  rfl

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

Goal state before:
pp: case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ (fun {α} ↦ η.app α) (Vector.traverse f (x✝ ::ᵥ w✝)) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) (x✝ ::ᵥ w✝)

Tactic:
rw [Vector.traverse_def, Vector.traverse_def, ← ih, η.preserves_seq, η.preserves_map]

Goal state after:
case cons
n : ℕ
F G : Type u → Type u
inst✝³ : Applicative F
inst✝² : Applicative G
inst✝¹ : LawfulApplicative G
inst✝ : LawfulApplicative F
η : ApplicativeTransformation F G
α β : Type u
f : α → F β
n✝ : ℕ
x✝ : α
w✝ : Vector α n✝
ih : (fun {α} ↦ η.app α) (Vector.traverse f w✝) = Vector.traverse ((fun {α} ↦ η.app α) ∘ f) w✝
⊢ cons <$> (fun {α} ↦ η.app α) (f x✝) <*> (fun {α} ↦ η.app α) (Vector.traverse f w✝) =
    cons <$> ((fun {α} ↦ η.app α) ∘ f) x✝ <*> (fun {α} ↦ η.app α) (Vector.traverse f w✝)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : OrderBot α
inst✝ : LE β
⊢ ∀ (a : α ⊕ₗ β), inl ⊥ ≤ a

Tactic:
rintro (a | b)
    · exact Lex.inl bot_le
    · exact Lex.sep _ _

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

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
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : (α ⊕ₗ β)ᵒᵈ
⊢ (Equiv.sumComm α β) a ≤ (Equiv.sumComm α β) b ↔ a ≤ b

Tactic:
rcases a with (a | a) <;> rcases b with (b | b)

Goal state after:
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inl b) ↔ inl a ≤ inl b

case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inr b) ↔ inl a ≤ inr b

case inr.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a : β
b : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ inl b

case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inr b) ↔ inr a ≤ inr b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f = g

Tactic:
rw [← toRelEmbedding_inj]

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f g : r ≺i s
h : ∀ (x : α), f.toRelEmbedding x = g.toRelEmbedding x
⊢ f.toRelEmbedding = g.toRelEmbedding
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ≺i s
g : s ≼i t
a : γ
⊢ a ∈ Set.range ⇑(f.trans g.toRelEmbedding) ↔ t a (g f.top)

Tactic:
by
    simp [g.exists_eq_iff_rel, ← PrincipalSeg.mem_range_iff_rel, exists_comm, ← exists_and_left]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
a : α
⊢ (↑(Option.some a)).Dom ↔ (Option.some a).isSome = true

Tactic:
simp [ofOption]

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl
α : 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
hzy : z ≤ y
⊢ f z ≤ y ∨ f y ≤ f z

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:
· rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)
        · left; exact hy.map_le_of_mem_of_lt hz hzy
        · right; exact le_refl _

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 z ≤ y ∨ f y ≤ f z
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ {a, b} ∈ Set.range fun c ↦ Set.range ⇑c

Tactic:
use pair a b hab

Goal state after:
case h
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
h : ωScottContinuous f
a b : α
hab : a ≤ b
⊢ (fun c ↦ Set.range ⇑c) (pair a b hab) = {a, b}
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
⊢ False

Tactic:
obtain h' | h' := ih c₃ hc₃ hc₁ h

Goal state after:
case union.inr.inl
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False

case union.inr.inr
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h✝ : c₁ ⊆ ⋃₀ s✝
c₃ : Set α
hc₃ : c₃ ∈ s✝
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s✝
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
β : α → Type u_6
inst✝ : (a : α) → OmegaCompletePartialOrder (β a)
x✝¹ : Chain ((a : α) → β a)
x✝ : (a : α) → β a
hf : ∀ (i : ℕ), x✝¹ i ≤ x✝
a : α
⊢ ∀ (i : ℕ), (x✝¹.map (Pi.evalOrderHom a)) i ≤ x✝ a

Tactic:
by
      rintro i
      apply hf

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

Goal state before:
pp: α β : Type u
⊢ ∀ (a : Cardinal.{u}), 0 ≤ a

Tactic:
by rintro ⟨α⟩; exact ⟨Embedding.ofIsEmpty⟩

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

Goal state before:
pp: a : Cardinal.{u}
⊢ 1 ≤ lift.{v, u} a ↔ 1 ≤ a

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

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

Goal state before:
pp: case coe
m : ℕ
hm : ↑m ≠ 0
⊢ ↑m * ℵ₀ = ℵ₀

Tactic:
nat_mul_aleph0 (mod_cast hm)

Goal state after:
case coe
m : ℕ
hm : ↑m ≠ 0
⊢ ℵ₀ = ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (lift.{u, w} '' range f) = sSup (range fun i ↦ lift.{u, w} (f i))

Tactic:
← range_comp

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift.{u, w} ∘ f)) = sSup (range fun i ↦ lift.{u, w} (f i))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
c : Cardinal.{u_1}
⊢ ↑n + 1 ≤ c ↔ ↑n < c

Tactic:
← Order.succ_le_iff,

Goal state after:
n : ℕ
c : Cardinal.{u_1}
⊢ ↑n + 1 ≤ c ↔ succ ↑n ≤ c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n < ℵ₀

Tactic:
rw [← natCast_add_one_le_iff, ← Nat.cast_add_one, ← lift_mk_fin, aleph0, lift_mk_le.{u}]
  exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩

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

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
⊢ #↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n

Tactic:
refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩

Goal state after:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
⊢ #↑t ≤ ↑n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
⊢ #↑A < #↑B

Tactic:
have : Fintype A := (hfin.subset hlt.subset).fintype

Goal state after:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this : Fintype ↑A
⊢ #↑A < #↑B
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: 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✝¹ : MulAction M α
inst✝ : MulAction M β
x✝² x✝¹ : M
x✝ : α × β
⊢ (x✝² * x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
ext <;> exact mul_smul ..

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective ⇑(f' * f' ^ n.pred)
⊢ Surjective ⇑f'

Tactic:
coe_mul

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
n : ℕ
hn : n ≠ 0
h : Surjective (⇑f' ∘ ⇑(f' ^ n.pred))
⊢ Surjective ⇑f'
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
change x ∈ ⋂ s ∈ Set.range p, s ↔ _

Goal state after:
R : Type u
M : Type v
inst✝ : SMul R M
ι : Sort u_1
p : ι → SubMulAction R M
x : M
⊢ x ∈ ⋂ s ∈ Set.range p, ↑s ↔ ∀ (i : ι), x ∈ p i
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a b : G₀
ha : a ∈ s.centralizer
hb : b ∈ s.centralizer
⊢ a / b ∈ s.centralizer

Tactic:
by
  simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer₀ hb)

Goal state after:
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝ : M
⊢ Commute (↑n) x✝

Tactic:
by rw [commute_iff_eq, Nat.commute_cast]

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
x : R × S
⊢ (fun x ↦ (x, 0)) x.1 = x

Tactic:
by cases x; simp [eq_iff_true_of_subsingleton]

Goal state after:
Module: Mathlib.Algebra.Ring.Prod

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
S' : Type u_4
T : Type u_5
inst✝⁴ : NonAssocSemiring R
inst✝³ : NonAssocSemiring S
inst✝² : NonAssocSemiring R'
inst✝¹ : NonAssocSemiring S'
inst✝ : Subsingleton S
x : S × R
⊢ (fun x ↦ (0, x)) x.2 = x

Tactic:
by cases x; simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : Semiring A
inst✝⁵ : Algebra R A
inst✝⁴ : FaithfulSMul R A
G : Type u_3
inst✝³ : Monoid G
inst✝² : MulSemiringAction G A
inst✝¹ : SMul G R
inst✝ : SMulDistribClass G R A
x✝ : G
⊢ x✝ • 0 = 0

Tactic:
apply FaithfulSMul.algebraMap_injective R A
    rw [algebraMap.smul', map_zero, smul_zero]

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

Goal state before:
pp: F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective
  simpa using (Set.injOn_of_injective hf).image_iInter_eq (s := SetLike.coe ∘ s)

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

Goal state before:
pp: case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = L.prod
⊢ C L.prod

Tactic:
clear HP HL hd

Goal state after:
case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
⊢ C L.prod
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C (-L.prod)

Tactic:
clear HP HL hd

Goal state after:
case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
L : List R
HL' : ∀ x ∈ L, x ∈ s
⊢ C (-L.prod)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero M₀'
r x y : M₀
inst✝¹ : Nontrivial M₀
inst✝ : IsLeftCancelMulZero M₀
z x✝¹ x✝ : ↥M₀⁰
h : (fun x ↦ z * x) x✝¹ = (fun x ↦ z * x) x✝
⊢ ↑z * ↑x✝¹ = ↑z * ↑x✝

Tactic:
simpa only [Subtype.ext_iff, Submonoid.coe_mul] using h

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝³ : MonoidWithZero M₀
inst✝² : MonoidWithZero M₀'
r x y : M₀
inst✝¹ : Nontrivial M₀
inst✝ : IsRightCancelMulZero M₀
z x✝¹ x✝ : ↥M₀⁰
h : (fun x ↦ x * z) x✝¹ = (fun x ↦ x * z) x✝
⊢ ↑x✝¹ * ↑z = ↑x✝ * ↑z

Tactic:
simpa only [Subtype.ext_iff, Submonoid.coe_mul] using h

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ M₀⁰ ↔ ∀ (x : M₀), r * x = 0 → x = 0

Tactic:
by
  rw [← nonZeroDivisorsLeft_eq_nonZeroDivisors]; rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
⊢ C x

Tactic:
have h0 : C 0 := add_neg_cancel (1 : R) ▸ ha h1 hneg1
  rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩
  clear hx
  induction L with
  | nil => exact h0
  | cons hd tl ih => ?_
  rw [List.forall_mem_cons] at HL
  suffices C (List.prod hd) by
    rw [List.map_cons, List.sum_cons]
    exact ha this (ih HL.2)
  replace HL := HL.1
  clear ih tl
  rsuffices ⟨L, HL', HP | HP⟩ :
    ∃ L : List R, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L)
  · rw [HP]
    clear HP HL hd
    induction L with
    | nil => exact h1
    | cons hd tl ih =>
      rw [List.forall_mem_cons] at HL'
      rw [List.prod_cons]
      exact hs _ HL'.1 _ (ih HL'.2)
  · rw [HP]
    clear HP HL hd
    induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)
  induction hd with
  | nil => exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩
  | cons hd tl ih => ?_
  rw [List.forall_mem_cons] at HL
  rcases ih HL.2 with ⟨L, HL', HP | HP⟩ <;> rcases HL.1 with hhd | hhd
  · exact
      ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩,
        Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩
  · exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩
  · exact
      ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩,
        Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩
  · exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩

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

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

Tactic:
closure_le

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
⊢ ⇑f '' ⇑f ⁻¹' {0} ⊆ ↑(map f s)
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
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ closure (⇑f ⁻¹' {0}) ≤ s

Tactic:
closure_le

Goal state after:
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
h : ⇑f ⁻¹' {0} ⊆ ↑s
⊢ ⇑f ⁻¹' {0} ⊆ ↑s
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✝⁵ : CommSemiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
c : R₂
⊢ (c • f).range ≤ f.range

Tactic:
simpa only [range_eq_map] using Submodule.map_smul_le_map _ _ _

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

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ x ∈ ϕ.submoduleImage N ↔ ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

Tactic:
refine Submodule.mem_map.trans ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y ∈ Submodule.comap O.subtype N, ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y ∈ Submodule.comap O.subtype N, ϕ y = x
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc b (a ⊔ b))
⊢ ↑x ⊓ a ⊔ b = ↑x

Tactic:
inf_sup_assoc_of_le _ x.prop.1,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc b (a ⊔ b))
⊢ ↑x ⊓ (a ⊔ b) = ↑x
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
S : Type u_7
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : SetLike S M
inst✝¹ : AddSubmonoidClass S M
inst✝ : SMulMemClass S R M
s : S
s' : Submodule R M := { carrier := ↑s, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
⊢ ↑(span R ↑s) ⊆ ↑s

Tactic:
exact span_le (p := s') |>.mpr le_rfl

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_9
inst✝² : SMul S R
inst✝¹ : SMul S M
inst✝ : IsScalarTower S R M
r : S
x : M
⊢ R ∙ r • x ≤ R ∙ x

Tactic:
rw [span_le, Set.singleton_subset_iff, SetLike.mem_coe]
  exact smul_of_tower_mem _ _ (mem_span_singleton_self _)

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
a : α
ha : a ∈ s
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
a : α
ha : a ∈ s
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
exact Or.inr ⟨a, hs _ ha, hsb.1 ha⟩

Goal state after: