mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ (f.domRestrict K).range = map f K

Tactic:
[

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
K : Subgroup G
f : G →* N
⊢ (f.domRestrict K).range = map f K
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
[

Goal state after:
G : Type u_1
inst✝¹ : Group G
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → Subgroup G
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a
Module: Mathlib.Algebra.Group.Subgroup.Ker

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K < comap f L ↔ K < L

Tactic:
[

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
K L : Subgroup N
hf : Surjective ⇑f
⊢ comap f K < comap f L ↔ K < L
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ z ∈ closure {x, y} ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
rw [← Set.singleton_union, Subgroup.closure_union, mem_sup]

Goal state after:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z
Module: Mathlib.Algebra.Group.Subgroup.Lattice

Goal state before:
pp: C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z

Tactic:
[

Goal state after:
C : Type u_2
inst✝ : CommGroup C
x y z : C
⊢ (∃ y_1 ∈ closure {x}, ∃ z_1 ∈ closure {y}, y_1 * z_1 = z) ↔ ∃ m n, x ^ m * y ^ n = z
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
[

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)
Module: Mathlib.Algebra.Group.Subsemigroup.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
[

Goal state after:
M : Type u_2
inst✝ : Mul M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
[

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set M
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)
Module: Mathlib.Algebra.Group.Submonoid.MulOpposite

Goal state before:
pp: M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
[

Goal state after:
M : Type u_2
inst✝ : MulOneClass M
s : Set Mᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥

Tactic:
[

Goal state after:
ι : Type u_4
M : ι → Type u_5
inst✝ : (i : ι) → MulOneClass (M i)
S : (i : ι) → Submonoid (M i)
⊢ pi Set.univ S = ⊥ ↔ ∀ (i : ι), S i = ⊥
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x : ↥(IsUnit.submonoid M)
⊢ ⟨↑(IsUnit.unit ⋯), ⋯⟩ = x

Tactic:
[

Goal state after:
M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x : ↥(IsUnit.submonoid M)
⊢ ⟨↑(IsUnit.unit ⋯), ⋯⟩ = x
Module: Mathlib.Algebra.Group.Submonoid.Operations

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑(x * y), ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩

Tactic:
[

Goal state after:
M✝ : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : MulOneClass M✝
inst✝² : MulOneClass N
inst✝¹ : MulOneClass P
S : Submonoid M✝
M : Type u_4
inst✝ : Monoid M
x y : Mˣ
⊢ ⟨↑(x * y), ⋯⟩ = ⟨↑x, ⋯⟩ * ⟨↑y, ⋯⟩
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: b : Bool
n : ℕ
⊢ bit b n / 2 = n

Tactic:
bit_div_two

Goal state after:
b : Bool
n : ℕ
⊢ n = n
Module: Mathlib.Data.Nat.Pairing

Goal state before:
pp: case pos
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : n - s * s < s
⊢ n - n.sqrt * n.sqrt < n

pp: case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n

Tactic:
· exact lt_of_lt_of_le h (sqrt_le_self _)

Goal state after:
case neg
n : ℕ
n1 : 1 ≤ n
s : ℕ := n.sqrt
h : ¬n - s * s < s
⊢ n.sqrt < n
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (decode (encode x)).getD d = x

Tactic:
[

Goal state after:
α : Type u_3
inst✝ : Encodable α
d x : α
⊢ (decode (encode x)).getD d = x
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)

Tactic:
[

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
⊢ (closure s).op = closure (MulOpposite.unop ⁻¹' s)
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)

Tactic:
[

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set Gᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' MulOpposite.op ⁻¹' s)
Module: Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas

Goal state before:
pp: G : Type u_2
inst✝ : Group G
H : Subgroup Gᵐᵒᵖ
⊢ H.unop.Normal ↔ H.Normal

Tactic:
rw [← normal_op, op_unop]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range encode

Tactic:
[

Goal state after:
α : Type u_1
inst✝ : Encodable α
n : ℕ
⊢ decode₂ α n ≠ none ↔ n ∈ Set.range encode
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ (decodeSum n).bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none

Tactic:
this

Goal state after:
n : ℕ
h : 2 ≤ n
this : decodeSum n = none
⊢ none.bind (some ∘ ⇑Equiv.boolEquivPUnitSumPUnit.symm) = none
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: n : ℕ
h : 2 ≤ n
⊢ 1 * 2 ≤ n

pp: n : ℕ
h : 2 ≤ n
⊢ 0 < 2

Tactic:
exacts [h, by decide]

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

Goal state before:
pp: η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi univ H = ⊥ ↔ ∀ (i : η), H i = ⊥

Tactic:
[

Goal state after:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
H : (i : η) → Subgroup (f i)
⊢ pi univ H = ⊥ ↔ ∀ (i : η), H i = ⊥
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H = H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H

Tactic:
simp_rw [map_equiv_eq_comap_symm']
  exact characteristic_iff_le_comap.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ g ∈ normalizer s ↔ ⇑(MulAut.conj g) '' s = s

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g : G
⊢ g ∈ normalizer s ↔ ⇑(MulAut.conj g) '' s = s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
s : Set G
g h : G
⊢ (h ∈ s ↔ g⁻¹ * h * g ∈ s) ↔ ((∃ x ∈ s, g * x * g⁻¹ = h) ↔ h ∈ s)
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Normal ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H

Tactic:
[

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Normal ↔ ∀ (g : G), map (↑(MulAut.conj g)) H = H
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ conjugatesOfSet (s ∪ t) = conjugatesOfSet s ∪ conjugatesOfSet t

Tactic:
[

Goal state after:
G : Type u_5
inst✝ : Group G
s t : Set G
⊢ conjugatesOfSet (s ∪ t) = conjugatesOfSet s ∪ conjugatesOfSet t
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_5
inst✝ : Group G
s t : Set G
⊢ normalClosure (s ∪ t) = normalClosure s ⊔ normalClosure t

Tactic:
[

Goal state after:
G : Type u_5
inst✝ : Group G
s t : Set G
⊢ normalClosure (s ∪ t) = normalClosure s ⊔ normalClosure t
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun x2 ↦ 1 • x2) '' s = s

Tactic:
[

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid α
inst✝ : MulAction α β
s : Set β
⊢ (fun x2 ↦ 1 • x2) '' s = s
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
| ⨅ g, map (↑(MulAut.conj g)) H

Tactic:
← Equiv.iInf_comp (Equiv.mulLeft g)

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
| ⨅ x, map (↑(MulAut.conj ((Equiv.mulLeft g) x))) H
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ a • sᶜ = (a • s)ᶜ

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
a : α
⊢ a • sᶜ = (a • s)ᶜ
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : Group α
s t : Set α
x : α
⊢ (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a / b = x
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g • s = {a | ∃ g, g • a ∈ s}

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g • s = {a | ∃ g, g • a ∈ s}
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ Pairwise (Disjoint on fun a ↦ a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1

Tactic:
[

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ Pairwise (Disjoint on fun a ↦ a • s) ↔ ∀ (a : α), (a • s ∩ s).Nonempty → a = 1
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩

Tactic:
[

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h = (f.liftOfRightInverse f_inv hf) ⟨g, hg⟩
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : Group α
s t : Set α
a b z : α
hzA : z ∈ a • s
hzB : z ∈ b • t
⊢ z • s⁻¹ * s ∩ (z • t⁻¹ * t) = z • (s⁻¹ * s ∩ (t⁻¹ * t))
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ a • s / b • t = (a / b) • (s / t)

Tactic:
[

Goal state after:
α : Type u_2
inst✝ : CommGroup α
a : α
s : Set α
b : α
t : Set α
⊢ a • s / b • t = (a / b) • (s / t)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a

Tactic:
[

Goal state after:
M : Type u_1
inst✝¹ : MulOneClass M
ι : Sort u_4
inst✝ : Nonempty ι
S : ι → Submonoid M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ ∀ a ∈ ⨆ i, S i, ∀ b ∈ ⨆ i, S i, a * b = b * a
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: case cons
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ (head✝ :: tail✝).prod

Tactic:
[

Goal state after:
case cons
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Preorder M
inst✝ : IsOrderedMonoid M
head✝ : M
tail✝ : List M
tail_ih✝ : (∀ (x : M), x ∈ tail✝ → 1 ≤ x) → ∀ (x : M), x ∈ tail✝ → x ≤ tail✝.prod
hl₁ : ∀ (x : M), x ∈ head✝ :: tail✝ → 1 ≤ x
⊢ ∀ (x : M), x ∈ head✝ :: tail✝ → x ≤ (head✝ :: tail✝).prod
Module: Mathlib.Logic.Embedding.Set

Goal state before:
pp: case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
⊢ ¬p ↑x

Tactic:
intro hp

Goal state after:
case inr.hx
α : Type u_1
p q : α → Prop
inst✝ : DecidablePred p
h : Disjoint p q
x : { x // q x }
hp : p ↑x
⊢ False
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : M
h : x ∈ closure s
⊢ motive x h

Tactic:
[

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
motive : (m : M) → m ∈ closure s → Prop
one : motive 1 ⋯
mul_left : ∀ (x : M) (hx : x ∈ s) (y : M) (hy : y ∈ closure s), motive y hy → motive (x * y) ⋯
x : M
h : x ∈ closure s
⊢ motive x h
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
z : ↥(powers x)
⊢ z ^ 0 = 1

Tactic:
[

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x : M
n : ℕ
hpos : 0 < n
hx : x ^ n = 1
z : ↥(powers x)
⊢ z ^ 0 = 1
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x✝ : M
n : ℕ
hpos : 0 < n
hx : x✝ ^ n = 1
m : ℕ
x : ↥(powers x✝)
⊢ ↑(x ^ ↑m.succ) = ↑(x ^ ↑m * x)

Tactic:
[

Goal state after:
M : Type u_1
A : Type u_2
B : Type u_3
inst✝ : Monoid M
a x✝ : M
n : ℕ
hpos : 0 < n
hx : x✝ ^ n = 1
m : ℕ
x : ↥(powers x✝)
⊢ ↑(x ^ ↑m.succ) = ↑(x ^ ↑m * x)
Module: Mathlib.Algebra.Group.Submonoid.Membership

Goal state before:
pp: A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c

Tactic:
[

Goal state after:
A : Type u_4
inst✝ : CommMonoid A
a b c : A
⊢ (∃ y ∈ closure {a}, ∃ z ∈ closure {b}, y * z = c) ↔ ∃ m n, a ^ m * b ^ n = c
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
x : α ⊕ β
⊢ x ∈ s.disjSum t ↔ (∃ a, a ∈ s ∧ inl a = x) ∨ ∃ b, b ∈ t ∧ inr b = x
Module: Mathlib.Data.Multiset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (s.disjSum t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Multiset α
t : Multiset β
f : α ⊕ β → γ
⊢ map f (s.disjSum t) = map (fun x ↦ f (inl x)) s + map (fun x ↦ f (inr x)) t
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ Disjoint (map Embedding.inl s) (map Embedding.inr t)
Module: Mathlib.Data.Finset.Sum

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ fold op (op b₁ b₂) f (s.disjSum t) = op (fold op b₁ (fun x ↦ f (inl x)) s) (fold op b₂ (fun x ↦ f (inr x)) t)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Finset α
t : Finset β
f : α ⊕ β → γ
b₁ b₂ : γ
op : γ → γ → γ
inst✝¹ : Std.Commutative op
inst✝ : Std.Associative op
⊢ fold op (op b₁ b₂) f (s.disjSum t) = op (fold op b₁ (fun x ↦ f (inl x)) s) (fold op b₂ (fun x ↦ f (inr x)) t)
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case nil
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ ↑a ≤ [].maximum ↔ ∃ b, b ∈ [] ∧ a ≤ b

Tactic:
simp [maximum_cons, *]

Goal state after:
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: case cons
α : Type u_1
inst✝ : LinearOrder α
l : List α
a head✝ : α
tail✝ : List α
tail_ih✝ : ↑a ≤ tail✝.maximum ↔ ∃ b, b ∈ tail✝ ∧ a ≤ b
⊢ ↑a ≤ (head✝ :: tail✝).maximum ↔ ∃ b, b ∈ head✝ :: tail✝ ∧ a ≤ b

Tactic:
simp [maximum_cons, *]

Goal state after:
Module: Mathlib.Logic.Denumerable

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
⊢ Denumerable α

Tactic:
letI := @decidableRangeEncode α _

Goal state after:
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝¹ : Encodable α
inst✝ : Infinite α
this : DecidablePred fun x ↦ x ∈ Set.range encode := decidableRangeEncode α
⊢ Denumerable α
Module: Mathlib.Order.Hom.Lattice

Goal state before:
pp: case inr
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : FunLike F α β
inst✝² : LinearOrder α
inst✝¹ : Lattice β
inst✝ : OrderHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ f (max a b) = f a ⊔ f b

Tactic:
rw [sup_eq_left.2 h, sup_eq_left.2 (OrderHomClass.mono f h : f b ≤ f a)]

Goal state after:
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.max = ↑a

Tactic:
by
  rw [← insert_empty_eq]
  exact max_insert

Goal state after:
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ [].inits.zip [].tails ↔ init ++ tail = []

Tactic:
[

Goal state after:
case nil
α : Type u
init tail : List α
⊢ (init, tail) ∈ [].inits.zip [].tails ↔ init ++ tail = []
Module: Mathlib.Data.List.Zip

Goal state before:
pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ (head✝ :: tail✝).inits.zip (head✝ :: tail✝).tails ↔ init ++ tail = head✝ :: tail✝

Tactic:
[

Goal state after:
case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ {init tail : List α}, (init, tail) ∈ tail✝.inits.zip tail✝.tails ↔ init ++ tail = tail✝
init tail : List α
⊢ (init, tail) ∈ (head✝ :: tail✝).inits.zip (head✝ :: tail✝).tails ↔ init ++ tail = head✝ :: tail✝
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) i

Tactic:
this

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
i : α
s : Finset α
hs : s.Nonempty
his : IsGLB (↑s) i
this : i = s.min' hs
⊢ IsLeast (↑s) (s.min' hs)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case succ
α : Type u
n : ℕ
IHn : ∀ {l₁ l₂ : List α}, l₁ <+ l₂ → sublistsLen n l₁ <+ sublistsLen n l₂
l₁ l₂ : List α
h : l₁ <+ l₂
⊢ sublistsLen (n + 1) l₁ <+ sublistsLen (n + 1) l₂

Tactic:
induction h with
  | slnil => rfl
  | cons a _ IH =>
    refine IH.trans ?_
    rw [sublistsLen_succ_cons]
    apply sublist_append_left
  | cons_cons a s IH => simpa only [sublistsLen_succ_cons] using IH.append ((IHn s).map _)

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: case h
α : Type u_2
a✝ : List α
⊢ ((range (card ⟦a✝⟧ + 1)).bind fun k ↦ powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧

Tactic:
[

Goal state after:
case h
α : Type u_2
a✝ : List α
⊢ ((range (card ⟦a✝⟧ + 1)).bind fun k ↦ powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'

Tactic:
[

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n (h :: tl)) (range ((h :: tl).length + 1)) ~ (h :: tl).sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
        flatMap (fun a ↦ map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
[

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
        flatMap (fun a ↦ map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] ::
      (flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
        flatMap (fun a ↦ map (cons h) (sublistsLen a tl)) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'

Tactic:
simp_rw [← List.map_flatMap, ← cons_append]

Goal state after:
case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ [] :: flatMap (fun a ↦ sublistsLen (a + 1) tl) (range (tl.length + 1)) ++
      map (cons h) (flatMap (fun a ↦ sublistsLen a tl) (range (tl.length + 1))) ~
    tl.sublists' ++ map (cons h) tl.sublists'