mathlib-initiative/mathlib-tactics huggingface dataset:
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_cases hx : x ∈ s

Goal state after:
case pos
ι : 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 : ι
hx : x ∈ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x

case neg
ι : 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 : ι
hx : x ∉ s
⊢ s.piecewise f g x ≤ s.piecewise f' g' x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

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

Tactic:
intro _ _ h
      rw [dif_neg]
      exact h.symm

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

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
fill : α
⊢ min n i + min (n - i) n = n

Tactic:
omega

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i, f ((Equiv.optionSubtypeNe a) i) = f a * ∏ i, f ↑i

Tactic:
prod_option,

Goal state after:
α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ f ((Equiv.optionSubtypeNe a) none) * ∏ i, f ((Equiv.optionSubtypeNe a) (some i)) = f a * ∏ i, f ↑i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ 0 + count a ↑m = count a ↑m

Tactic:
zero_add

Goal state after:
case inl
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
⊢ count a ↑m = count a ↑m
Module: Mathlib.Data.Set.Countable

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

Tactic:
rintro ⟨s, hps, hs⟩

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ (f ⁻¹' univ).Countable

Tactic:
← Set.iUnion_of_singleton,

Goal state after:
α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ (f ⁻¹' ⋃ x, {x}).Countable
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
    contrapose! hlim
    rw [csSup_of_not_bddAbove hlim, csSup_empty]
    exact isSuccPrelimit_bot

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Defs

Goal state before:
pp: α : Type u_1
f g : α → α
⊢ fixedPoints f ∩ fixedPoints g ⊆ fixedPoints (f ∘ g)

Tactic:
rintro x ⟨hf, hg⟩

Goal state after:
α : Type u_1
f g : α → α
x : α
hf : x ∈ fixedPoints f
hg : x ∈ fixedPoints g
⊢ x ∈ fixedPoints (f ∘ g)
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∉ Set.range ⇑f
hs : s y x
⊢ ∃ a, f a = x

Tactic:
obtain ⟨z, rfl⟩ := IH y hs

Goal state after:
case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
z : α
hy : f z ∉ Set.range ⇑f
hs : s (f z) x
⊢ ∃ a, f a = x
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Union α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ∪ mb ∈ a ∪ b

Tactic:
by simp [union_def]; aesop

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ f (ωSup c) >>= g (ωSup c) = ωSup (c.map { toFun := fun x ↦ f x >>= g x, monotone' := ⋯ })

Tactic:
rw [hf.map_ωSup, hg.map_ωSup, ← ωSup_bind]; rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ (c₀ i) (c₁ (max i j)) ≤ (c₀ (max i j)) (c₁ (max i j))

Tactic:
apply c₀.monotone
      apply le_max_left

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

Goal state before:
pp: case mk.mk
α✝ β✝ : Type u
a✝ : Cardinal.{u}
α : Type u
b✝ : Cardinal.{u}
β : Type u
⊢ Quot.mk (⇑isEquivalent) α ≤ Quot.mk (⇑isEquivalent) β ∨ Quot.mk (⇑isEquivalent) β ≤ Quot.mk (⇑isEquivalent) α

Tactic:
apply Embedding.total

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

Goal state before:
pp: α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift '' (fun x ↦ { down := f x.down }) ⁻¹' {{ down := b }}) ≃ ↑(f ⁻¹' {b})

Tactic:
rw [Equiv.image_eq_preimage_symm]
                  simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_ofPred_eq, coe_ofPred]
                  exact Equiv.refl _

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

Goal state before:
pp: α β : Type u
a b : ℕ
h : ↑a = ↑b
⊢ a = b

Tactic:
← lift_mk_fin,

Goal state after:
α β : Type u
a b : ℕ
h : lift.{u_1, 0} #(Fin a) = ↑b
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
a b : ℕ
h : lift.{u_1, 0} #(Fin a) = ↑b
⊢ a = b

Tactic:
← lift_mk_fin,

Goal state after:
α β : Type u
a b : ℕ
h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inl
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ℵ₀ ≤ c
hd : ℵ₀ ≤ d
⊢ toNat c = toNat d

pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d

Tactic:
· simp [Cardinal.toNat_apply_of_aleph0_le, hc, hd]

Goal state after:
case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
j : Cardinal.{u_1}
hj : j ∈ s
⊢ lift.{u, u_1} j ≤ lift.{u, u_1} (sSup s)

Tactic:
exact lift_le.2 (le_csSup hs hj)

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

Goal state before:
pp: n : ℕ
⊢ ↑(n + 1) ≤ ℵ₀

Tactic:
← lift_mk_fin,

Goal state after:
n : ℕ
⊢ lift.{u, 0} #(Fin (n + 1)) ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
exact not_isSuccLimit_natCast n

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ Nonempty (α ≃ Fin n)

Tactic:
← lift_mk_fin,

Goal state after:
α : Type u
n : ℕ
⊢ #α = lift.{u, 0} #(Fin n) ↔ Nonempty (α ≃ Fin n)
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ r • a • 1 = r • 1

Tactic:
smul_one

Goal state after:
R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ r • 1 = r • 1
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
tF : A →ₑ[⇑φ] B
map_one'✝¹ : tF.toFun 1 = 1
map_mul'✝¹ : ∀ (x y : A), tF.toFun (x * y) = tF.toFun x * tF.toFun y
tG : A →ₑ[⇑φ] B
map_one'✝ : tG.toFun 1 = 1
map_mul'✝ : ∀ (x y : A), tG.toFun (x * y) = tG.toFun x * tG.toFun y
h :
  (fun m ↦ m.toFun) { toMulActionHom := tF, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    (fun m ↦ m.toFun) { toMulActionHom := tG, map_one' := map_one'✝, map_mul' := map_mul'✝ }
⊢ { toMulActionHom := tF, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ } =
    { toMulActionHom := tG, map_one' := map_one'✝, map_mul' := map_mul'✝ }

Tactic:
cases tF

Goal state after:
case mk
M : Type u_1
inst✝¹⁴ : Monoid M
N : Type u_2
inst✝¹³ : Monoid N
P : Type u_3
inst✝¹² : Monoid P
φ : M →* N
φ' : N →* M
ψ : N →* P
χ : M →* P
A : Type u_4
inst✝¹¹ : Monoid A
inst✝¹⁰ : MulDistribMulAction M A
B : Type u_5
inst✝⁹ : Monoid B
inst✝⁸ : MulDistribMulAction N B
B₁ : Type u_6
inst✝⁷ : Monoid B₁
inst✝⁶ : MulDistribMulAction M B₁
C : Type u_7
inst✝⁵ : Monoid C
inst✝⁴ : MulDistribMulAction P C
A' : Type u_8
inst✝³ : Group A'
inst✝² : MulDistribMulAction M A'
B' : Type u_9
inst✝¹ : Group B'
inst✝ : MulDistribMulAction N B'
tG : A →ₑ[⇑φ] B
map_one'✝¹ : tG.toFun 1 = 1
map_mul'✝¹ : ∀ (x y : A), tG.toFun (x * y) = tG.toFun x * tG.toFun y
toFun✝ : A → B
map_smul'✝ : ∀ (m : M) (x : A), toFun✝ (m • x) = φ m • toFun✝ x
map_one'✝ : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun x * { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun y
h :
  (fun m ↦ m.toFun) { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    (fun m ↦ m.toFun) { toMulActionHom := tG, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }
⊢ { toFun := toFun✝, map_smul' := map_smul'✝, map_one' := map_one'✝, map_mul' := map_mul'✝ } =
    { toMulActionHom := tG, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }
Module: Mathlib.Algebra.Ring.Pi

Goal state before:
pp: I : Type u
f : I → Type v
i : I
inst✝ : (i : I) → Distrib (f i)
a✝ b✝ c✝ : (i : I) → f i
x✝ : I
⊢ ((a✝ + b✝) * c✝) x✝ = (a✝ * c✝ + b✝ * c✝) x✝

Tactic:
exact add_mul _ _ _

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

Goal state before:
pp: R : Type u_1
R' : Type u_2
S : Type u_3
M : Type u_4
M' : Type u_5
inst✝¹² : Semiring R
inst✝¹¹ : Semiring R'
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : Module R' M'
σ₁₂ : R →+* R'
S' : Type u_6
T' : Type u_7
inst✝⁶ : Monoid S'
inst✝⁵ : DistribMulAction S' M
inst✝⁴ : SMulCommClass R S' M
inst✝³ : Monoid T'
inst✝² : DistribMulAction T' M
inst✝¹ : SMulCommClass R T' M
inst✝ : SMulCommClass S' T' M
s : S'ᵈᵐᵃ
t : T'ᵈᵐᵃ
f : M →ₛₗ[σ₁₂] M'
m : M
⊢ f (DomMulAct.mk.symm t • DomMulAct.mk.symm s • m) = f (DomMulAct.mk.symm s • DomMulAct.mk.symm t • m)

Tactic:
smul_comm

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
h : Bijective ⇑f'
n : ℕ
⊢ Bijective ⇑(f' ^ (n + 1))

Tactic:
by
    rw [iterate_succ]
    exact (iterate_bijective h n).comp h

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton ↥p ↔ p = ⊥

Tactic:
rw [subsingleton_iff, Submodule.eq_bot_iff]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ (∀ (x y : ↥p), x = y) ↔ ∀ x ∈ p, x = 0
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ MulAction.stabilizer R m = MulAction.stabilizer R ↑m

Tactic:
by
  rw [← Subgroup.toSubmonoid_inj]
  exact stabilizer_of_subMul.submonoid m

Goal state after:
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₂
inst✝¹ : RingHomSurjective σ₁₂
ι : Sort u_9
inst✝ : Nonempty ι
p : ι → Submodule R M
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
⊢ ↑(map f (⨅ i, p i)) = ↑(⨅ i, map f (p i))

Tactic:
simpa only [map_coe, coe_iInf] using hf.injOn.image_iInter_eq

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : Subring R
⊢ S.toNonUnitalSubring.toSubring ⋯ = S

Tactic:
by cases S; rfl

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

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ (S.toSubring h1).toNonUnitalSubring = S

Tactic:
by cases S; rfl

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ x✝¹ * x✝ * 0 = x✝¹ * (x✝ * 0)

Tactic:
by rw [mul_zero, mul_zero, mul_zero]

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✝ • 1 = 1

Tactic:
smul_one

Goal state after:
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
⊢ 1 = 1
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
⊢ y ∈ ↑H.toAddSubmonoid

Tactic:
refine (Submonoid.mem_closure.mp hy) H.toSubmonoid fun z hz => ?_

Goal state after:
R : Type u
inst✝ : NonAssocSemiring R
s : Set R
x : R
hx : x ∈ closure ↑(AddSubmonoid.closure s)
H : Subsemiring R
J : H ∈ {S | s ⊆ ↑S}
y : R
hy : y ∈ ↑(Submonoid.closure ↑(AddSubmonoid.closure s))
z : R
hz : z ∈ ↑(AddSubmonoid.closure s)
⊢ z ∈ ↑H.toSubmonoid
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Tactic:
rintro ⟨L, HL1, rfl⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
L : List (List R)
HL1 : ∀ t ∈ L, ∀ y ∈ t, y ∈ s
⊢ (List.map List.prod L).sum ∈ closure s
Module: Mathlib.Algebra.Prime.Defs

Goal state before:
pp: case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ a ^ 0
⊢ p ∣ a

Tactic:
rw [pow_zero] at h

Goal state after:
case zero
M : Type u_1
inst✝ : CommMonoidWithZero M
p : M
hp : Prime p
a : M
h : p ∣ 1
⊢ p ∣ a
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
x : R
hy : e x ∈ s
⊢ ↑e.symm (e x) ∈ s'

Tactic:
simp [(h _).2 hy]

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case refine_1
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f a → p ∣ a

Tactic:
intro h
        convert! ← map_dvd g h <;> apply hinv

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case refine_2
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h : p ∣ a * b
⊢ f p ∣ f b → p ∣ b

Tactic:
intro h
        convert! ← map_dvd g h <;> apply hinv

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
⊢ s * 0 ⊆ 0

Tactic:
simp [subset_def, mem_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : MulZeroClass α
s : Set α
⊢ 0 * s ⊆ 0

Tactic:
simp [subset_def, mem_mul]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
⊢ map p.subtype p₁ ≤ map p.subtype p₂ ↔ p₁ ≤ p₂

Tactic:
rw [map_le_iff_le_comap,
      comap_map_eq_of_injective (show Injective p.subtype from Subtype.coe_injective) p₂]

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
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ ¬H ≤ K) ∧ H ≤ L ∧ H ≠ L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Tactic:
and_and_and_comm

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
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
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ K ≠ H) ∧ H ≤ L ∧ ¬L ≤ H ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Tactic:
and_and_and_comm

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
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
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Tactic:
by
  refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_
  push Not
  rw [lt_iff_le_and_ne, lt_iff_le_not_ge, and_and_and_comm]
  simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_2.inl.hnc
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
con : ⊤ ∈ s
⊢ False

Tactic:
exact bot_ne_top (eq_top_iff.2 (h con))

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i ↦ (g i).sup fun b ↦ f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b ↦ f ⟨i, b⟩
⊢ (s.sigma g).SupIndep f

Tactic:
classical
  rw [Finset.sigma_eq_biUnion]
  apply Finset.SupIndep.biUnion
  · simpa using! hs
  · simpa [Finset.supIndep_map] using! hg

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
s : Set α
⊢ (∃ x, s = {x}) → IsAtom s

Tactic:
by
      rintro ⟨x, rfl⟩
      exact isAtom_singleton x

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
h : ∀ (i : { i // t i ≠ ⊥ }), Disjoint (t ↑i) (⨆ j, ⨆ (_ : j ≠ i), t ↑j)
i : ι
hi : t i = ⊥
⊢ Disjoint (t i) (⨆ j, ⨆ (_ : j ≠ i), t j)

Tactic:
| inl hi =>

Goal state after:
Module: Mathlib.Data.FunLike.IsApply

Goal state before:
pp: case succ
F : Type u_1
α : Type u_2
inst✝³ : FunLike F α α
inst✝² : Monoid F
inst✝¹ : IsOneApplyEqSelf F α
inst✝ : IsMulApplyEqComp F α
f : F
x : α
n : ℕ
ih : (f ^ n) x = (⇑f)^[n] x
⊢ (f ^ (n + 1)) x = (⇑f)^[n + 1] x

Tactic:
simp [pow_succ', ih, ← Function.iterate_succ_apply']

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

Goal state before:
pp: case inr
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

Tactic:
have ⟨a, ba, h⟩ := zorn_le_nonempty₀ (Set.Iio k) ?_ b (lt_of_le_of_ne hbk H)

Goal state after:
case inr.refine_2
α : Type u_2
inst✝ : CompleteLattice α
k : α
h✝ : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
a : α
ba : b ≤ a
h : Maximal (fun x ↦ x ∈ Iio k) a
⊢ ∃ a, IsCoatom a ∧ ⟨b, hbk⟩ ≤ a

case inr.refine_1
α : Type u_2
inst✝ : CompleteLattice α
k : α
h : IsCompactElement k
b : α
hbk : b ∈ Iic k
H : b ≠ k
⊢ ∀ c ⊆ Iio k, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ Iio k, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case neg
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
ι : Type u_3
κ : ι → Type u_4
f : (i : ι) → κ i → α
h_indep : ∀ (i : ι), iSupIndep (f i)
s : Finset ((i : ι) → κ i)
ih : ∀ t ⊂ s, t.SupIndep fun k ↦ ⨅ i, f i (k i)
hs : ¬1 < s.card
⊢ s.SupIndep fun k ↦ ⨅ i, f i (k i)

Tactic:
by_cases hcard0 : s.card = 0 <;> grind [Finset.card_eq_zero, Finset.card_eq_one]

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

Goal state before:
pp: case smul_right
R : Type u_9
M : Type u_10
N : Type u_11
P : Type u_12
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
P' : Submodule R P
s : Set M
t✝ : Set N
B : M →ₗ[R] N →ₗ[R] P
hB : ∀ x ∈ s, ∀ y ∈ t✝, (B x) y ∈ P'
x : M
y : N
t : R
u : M
v : N
hu : u ∈ span R s
hv : v ∈ span R t✝
huv : (B u) v ∈ P'
⊢ (B u) (t • v) ∈ P'

Tactic:
| smul_right t u v hu hv huv =>

Goal state after: