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

Goal state before:
pp: case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∏ x ∈ t, x ^ f x = ∏ x ∈ t ∪ u, x ^ f x

Tactic:
refine Finset.prod_subset Finset.subset_union_left ?_

Goal state after:
case mul.e_a
M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
f : M → ℕ
t : Finset M
hts : ↑t ⊆ s
hf : Function.support f ⊆ ↑t
hx✝ : ∏ a ∈ t, a ^ f a ∈ closure s
g : M → ℕ
u : Finset M
hus : ↑u ⊆ s
hg : Function.support g ⊆ ↑u
hy✝ : ∏ a ∈ u, a ^ g a ∈ closure s
⊢ ∀ x ∈ t ∪ u, x ∉ t → x ^ f x = 1
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Setoid α
h : ∀ (x y : α), r x y → s x y
⊢ EqvGen.setoid r ≤ s

Tactic:
rw [eqvGen_eq]; exact sInf_le h

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f g : ι → M
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₁.prod f = s₂.prod g

Tactic:
h

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝ : CommMonoid M
f g : ι → M
h : s₁ = s₂
⊢ (∀ x ∈ s₂, f x = g x) → s₂.prod f = s₂.prod g
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f g : ι → M
inst✝ : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = (∏ x ∈ s₂ \ s₁, g x) * ∏ x ∈ s₁, g x

Tactic:
prod_eq_one hg,

Goal state after:
ι : Type u_1
M : Type u_4
s₁ s₂ : Finset ι
inst✝¹ : CommMonoid M
f g : ι → M
inst✝ : DecidableEq ι
h : s₁ ⊆ s₂
hg : ∀ x ∈ s₂ \ s₁, g x = 1
hfg : ∀ x ∈ s₁, f x = g x
⊢ ∏ i ∈ s₁, f i = 1 * ∏ x ∈ s₁, g x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ n, L₁.length = L₂.length + 2 * n

Tactic:
induction h with

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

Goal state before:
pp: α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ ((a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2) ∧ IsReduced ((a₂, b₂) :: L₁)

Tactic:
refine ⟨?_, .of_forall_not_step fun L₂ step ↦ hL₁ _ step.cons⟩

Goal state after:
α : Type u
a₁ : α
b₁ : Bool
a₂ : α
b₂ : Bool
L₁ : List (α × Bool)
hL₁ : ∀ (L₂ : List (α × Bool)), ¬Red.Step ((a₁, b₁) :: (a₂, b₂) :: L₁) L₂
⊢ (a₁, b₁).1 = (a₂, b₂).1 → (a₁, b₁).2 = (a₂, b₂).2
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
⊢ Red.Step a b → Red.Step (invRev a) (invRev b)

Tactic:
h

Goal state after:
α : Type u
L L₁ L₂ L₃ L₄ a b : List (α × Bool)
h : Red.Step a b
⊢ Red.Step (invRev a) (invRev b)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure (⇑e '' ↑(s.preimage ⇑e ⋯)) = closure ↑s

Tactic:
Finset.coe_preimage

Goal state after:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure (⇑e '' ⇑e ⁻¹' ↑s) = closure ↑s
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝ : Monoid M
s : Finset M
⊢ FG ↥(Submonoid.closure ↑s)

Tactic:
refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝ : Monoid M
s : Finset M
⊢ Submonoid.closure ↑(s.preimage Subtype.val ⋯) = ⊤
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
refine ⟨⟨s.preimage Subtype.val Subtype.coe_injective.injOn, ?_⟩⟩

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
s : Finset G
⊢ Subgroup.closure ↑(s.preimage Subtype.val ⋯) = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
f : κ → M
g : ι → κ
⊢ ∏ a ∈ s, f (g a) = ∏ x ∈ image g s, ∏ _x ∈ s with g _x = x, f x

Tactic:
prod_fiberwise_of_maps_to' fun _ ↦ mem_image_of_mem _

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

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f x = 1

Tactic:
h

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f a = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : x ∈ s
h : x = a
⊢ f a = 1

Tactic:
h

Goal state after:
case pos
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
hp : ∏ x ∈ s, f x = 1
h1 : ∀ x ∈ s, x ≠ a → f x = 1
x : ι
hx : a ∈ s
h : x = a
⊢ f a = 1
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ m * ↑s = n * ↑s

Tactic:
h

Goal state after:
R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ n * ↑s = n * ↑s
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
⊢ ∀ h ∈ ↑H₃, ⁅h, ⁅x, y⁆⁆ = 1

Tactic:
z

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
⊢ z ∈ ↑H₃ → ⁅z, ⁅x, y⁆⁆ = 1
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * (↑t * r) * r₂ = r₁' * (↑t * r') * r₂

Tactic:
h

Goal state after:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r r' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * (↑t * r') * r₂ = r₁' * (↑t * r') * r₂
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
C : Sort u_2
P : X → ↥S → X → ↥S → C
hP :
  ∀ (r₁ : X) (t₁ : R) (s₁ : ↥S) (ht₁ : t₁ * ↑s₁ ∈ S) (r₂ : X) (t₂ : R) (s₂ : ↥S) (ht₂ : t₂ * ↑s₂ ∈ S),
    P r₁ s₁ r₂ s₂ = P (t₁ • r₁) ⟨t₁ * ↑s₁, ht₁⟩ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩
r₁ : X
s₁ : ↥S
r₂ : X
t₂ : R
s₂ : ↥S
ht₂ : t₂ * ↑s₂ ∈ S
⊢ P r₁ s₁ r₂ s₂ = P r₁ s₁ (t₂ • r₂) ⟨t₂ * ↑s₂, ht₂⟩

Tactic:
by
      have := hP r₁ 1 s₁ (by simp) r₂ t₂ s₂ ht₂
      simp [this]

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

Goal state before:
pp: case refine_1
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {x y z : M × ↥S},
    (∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)) →
      (∃ c, ↑c * (↑z.2 * y.1) = ↑c * (↑y.2 * z.1)) → ∃ c, ↑c * (↑z.2 * x.1) = ↑c * (↑x.2 * z.1)

pp: case refine_2
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {w x y z : M × ↥S},
    (∃ c, ↑c * (↑x.2 * w.1) = ↑c * (↑w.2 * x.1)) →
      (∃ c, ↑c * (↑z.2 * y.1) = ↑c * (↑y.2 * z.1)) → ∃ c, ↑c * (↑(x * z).2 * (w * y).1) = ↑c * (↑(w * y).2 * (x * z).1)

Tactic:
· rintro a b c ⟨t₁, ht₁⟩ ⟨t₂, ht₂⟩
    use t₂ * t₁ * b.2
    simp only [Submonoid.coe_mul]
    calc
      (t₂ * t₁ * b.2 : M) * (c.2 * a.1) = t₂ * c.2 * (t₁ * (b.2 * a.1)) := by ac_rfl
      _ = t₁ * a.2 * (t₂ * (c.2 * b.1)) := by rw [ht₁]; ac_rfl
      _ = t₂ * t₁ * b.2 * (a.2 * c.1) := by rw [ht₂]; ac_rfl

Goal state after:
case refine_2
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
⊢ ∀ {w x y z : M × ↥S},
    (∃ c, ↑c * (↑x.2 * w.1) = ↑c * (↑w.2 * x.1)) →
      (∃ c, ↑c * (↑z.2 * y.1) = ↑c * (↑y.2 * z.1)) → ∃ c, ↑c * (↑(x * z).2 * (w * y).1) = ↑c * (↑(w * y).2 * (x * z).1)
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
h : ↑y.2 * x.1 = ↑x.2 * y.1
⊢ ↑1 * (↑y.2 * x.1) = ↑1 * (↑x.2 * y.1)

Tactic:
h

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
x y : M × ↥S
h : ↑y.2 * x.1 = ↑x.2 * y.1
⊢ ↑1 * (↑x.2 * y.1) = ↑1 * (↑x.2 * y.1)
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
⊢ Injective ⇑(f.lift hg)

Tactic:
z

Goal state after:
case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z : N
⊢ ∀ ⦃a₂ : N⦄, (f.lift hg) z = (f.lift hg) a₂ → z = a₂
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
⊢ (f.lift hg) z = (f.lift hg) w → z = w

Tactic:
h

Goal state after:
case mpr
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)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
h : (f.lift hg) z = (f.lift hg) w
⊢ z = w
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑z * ↑((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = 1

Tactic:
h

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : M →* N
hf : ∀ (y : ↥S), IsUnit (f ↑y)
y z : ↥S
h : ((IsUnit.liftRight (f.domRestrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹
⊢ f ↑z * ↑((IsUnit.liftRight (f.domRestrict S) hf) z)⁻¹ = 1
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f (x * ↑c) = f (y * ↑c)
⊢ f (x * ↑c) = f (y * ↑c)

Tactic:
h

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x y : M
c : ↥S
h : f (x * ↑c) = f (y * ↑c)
⊢ f (y * ↑c) = f (y * ↑c)
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
y : P
s : M
hs : s ∈ ↑S
ht : g s ∈ T
⊢ ∃ a, (f.map hy k) a = k.mk' y ⟨g s, ht⟩

Tactic:
obtain ⟨x, rfl⟩ := hg y

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
surj : Set.SurjOn ⇑g ↑S ↑T
hg : Surjective ⇑g
s : M
hs : s ∈ ↑S
ht : g s ∈ T
x : M
⊢ ∃ a, (f.map hy k) a = k.mk' (g x) ⟨g s, ht⟩
Module: Mathlib.Algebra.Order.Hom.Ring

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f₁ f₂ : β →+*o γ
g : α →+*o β
hg : Surjective ⇑g
h : f₁ = f₂
⊢ f₁.comp g = f₂.comp g

Tactic:
h

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : NonAssocSemiring α
inst✝⁴ : Preorder α
inst✝³ : NonAssocSemiring β
inst✝² : Preorder β
inst✝¹ : NonAssocSemiring γ
inst✝ : Preorder γ
f₁ f₂ : β →+*o γ
g : α →+*o β
hg : Surjective ⇑g
h : f₁ = f₂
⊢ f₂.comp g = f₂.comp g
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g

Tactic:
h

Goal state after:
R : Type u_7
S : Type u_8
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : NonUnitalNonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑g = ↑g
Module: Mathlib.Algebra.Ring.Equiv

Goal state before:
pp: R : Type u_7
S : Type u_8
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑f = ↑g

Tactic:
h

Goal state after:
R : Type u_7
S : Type u_8
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f g : R ≃+* S
h : f = g
⊢ ↑g = ↑g
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
⊢ (∀ ⦃a₁ a₂ : M⦄, f a₁ = f a₂ → a₁ = a₂) ↔ ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂

Tactic:
LocalizationMap.eq_iff_exists,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
⊢ (∀ ⦃a₁ a₂ : M⦄, (∃ c, ↑c * a₁ = ↑c * a₂) → a₁ = a₂) ↔ ∀ ⦃x : M⦄, x ∈ S → ∀ ⦃a₁ a₂ : M⦄, x * a₁ = x * a₂ → a₁ = a₂
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ (r • m • 1) • x = m • r • x

Tactic:
smul_comm,

Goal state after:
R : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹³ : Monoid M
S : Submonoid M
inst✝¹² : OreSet S
inst✝¹¹ : MulAction M X
inst✝¹⁰ : SMul R X
inst✝⁹ : SMul R M
inst✝⁸ : IsScalarTower R M M
inst✝⁷ : IsScalarTower R M X
inst✝⁶ : SMul R' X
inst✝⁵ : SMul R' M
inst✝⁴ : IsScalarTower R' M M
inst✝³ : IsScalarTower R' M X
inst✝² : SMul R R'
inst✝¹ : IsScalarTower R R' M
inst✝ : SMulCommClass R R' M
r : R
m : R'
x : OreLocalization S X
⊢ (m • r • 1) • x = m • r • x
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 < x2) a b

Tactic:
h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : (fun x y ↦ ↑x * y) ⟨x, x0⟩ a < (fun x y ↦ ↑x * y) ⟨x, x0⟩ b
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 < x2) a b

Tactic:
h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
h : (fun x y ↦ y * ↑x) ⟨x, x0⟩ a < (fun x y ↦ y * ↑x) ⟨x, x0⟩ b
⊢ a < b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : (fun x y ↦ ↑x * y) ⟨x, x0⟩ a ≤ (fun x y ↦ ↑x * y) ⟨x, x0⟩ b
⊢ a ≤ b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
h

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : (fun x y ↦ y * ↑x) ⟨x, x0⟩ a ≤ (fun x y ↦ y * ↑x) ⟨x, x0⟩ b
⊢ a ≤ b
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
x : α
h : IsSuccLimit x
⊢ IsSuccLimit ↑x

Tactic:
by
  simpa [isSuccLimit_iff, WithTop.exists, h.isSuccPrelimit.withTopCoe] using h.not_isMin

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

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Nonempty α
inst✝³ : Preorder β
f : α → β
inst✝² : NoMaxOrder α
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
hf : StrictMono f
m : β
hm : m ∈ upperBounds (Set.range f)
hm' : ∀ (a : α), f a ≤ m
a₀ : α
h : ∀ (a : α), ∃ a', f a < f a'
b : β
hmn✝ : f a₀ ≤ b
a : α
hba : b < f a
⊢ ∃ a, succ b < f a

Tactic:
exact (h a).imp (fun a' ↦ (succ_le_of_lt hba).trans_lt)

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

Goal state before:
pp: case pos
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : IsMax a
⊢ succ a < b

Tactic:
h.succ_eq

Goal state after:
case pos
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : IsMax a
⊢ a < b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h' : pred x ∈ s
h : ⟨x, hx⟩ ≤ ⟨pred x, h'⟩
⊢ IsMin ⟨x, hx⟩

Tactic:
simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h
      rintro ⟨y, _⟩ hy
      simp [h hy]

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

Goal state before:
pp: a b c d m n : ℕ∞
α : Type u_1
S : Type u_2
inst✝² : MulZeroOneClass S
inst✝¹ : DecidableEq S
inst✝ : Nontrivial S
f : ℕ →*₀ S
hf : Injective ⇑f
x y : ℕ∞
⊢ map (⇑f) (x * y) = map (⇑f) x * map (⇑f) y

Tactic:
have : ∀ z, map f z = 0 ↔ z = 0 := fun z =>
        (WithTop.map_injective hf).eq_iff' f.toZeroHom.ENatMap.map_zero
      rcases Decidable.eq_or_ne x 0 with (rfl | hx)
      · simp
      rcases Decidable.eq_or_ne y 0 with (rfl | hy)
      · simp
      induction x with
      | top => simp [hy, this]
      | coe x =>
        induction y with
        | top =>
          have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
          simp [mul_top hx, WithTop.mul_top this]
        | coe y => simp [← Nat.cast_mul, -natCast_mul]

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]

Goal state after:
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

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
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1
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✝ : ι
a✝ : b✝ ∈ s
⊢ b✝ ≠ a → (if h : a = b✝ then b b✝ h else 1) = 1

Tactic:
h

Goal state after:
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✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : a = b✝ then b b✝ h else 1) = 1
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 : ι) → x = a → M
h : a ∈ s
⊢ (∏ x ∈ s, if h : x = a then b x h else 1) = b a ⋯

Tactic:
rw [Finset.prod_eq_single a, dif_pos rfl]

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

case pos.h₁
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h : a ∈ s
⊢ a ∉ s → (if h : a = a then b a h else 1) = 1
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 : ι) → x = a → M
h : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
⊢ b✝ ≠ a → (if h : b✝ = a then b b✝ h else 1) = 1

Tactic:
h

Goal state after:
case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h✝ : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : b✝ = a then b b✝ h else 1) = 1
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u_1 → Type u_2
AF : Applicative F
inst✝ : LawfulApplicative F
α✝ β✝ : Type u_1
f : F (α✝ → β✝)
x : F α✝
⊢ id <$> f <*> x = f <*> x

Tactic:
id_map

Goal state after:
F : Type u_1 → Type u_2
AF : Applicative F
inst✝ : LawfulApplicative F
α✝ β✝ : Type u_1
f : F (α✝ → β✝)
x : F α✝
⊢ f <*> x = f <*> x
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
⊢ ¬(v.head = a ∧ v.tail = v') ↔ v.head ≠ a ∨ v.tail ≠ v'

Tactic:
not_and_or

Goal state after:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
⊢ ¬v.head = a ∨ ¬v.tail = v' ↔ v.head ≠ a ∨ v.tail ≠ v'
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

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

Tactic:
have ⟨y, hy⟩ := not_forall_not.mp hlim
    have ⟨i, his, hi⟩ := exists_lt_of_lt_csSup hne hy.lt
    exact eq_of_le_of_not_lt (le_csSup hbdd his) (hy.2 hi) ▸ his

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

Goal state before:
pp: α : Type u_1
f g : α → α
x : α
hf : x ∈ fixedPoints f
hg : x ∈ fixedPoints g
⊢ x ∈ fixedPoints (f ∘ g)

Tactic:
rw [mem_fixedPoints_iff] at *

Goal state after:
α : Type u_1
f g : α → α
x : α
hf : f x = x
hg : g x = x
⊢ (f ∘ g) x = x