mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: case inl
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
hny : y - 1 • a ∈ Ioc l (l + a)
hn : 1 ≤ 1
hy : R (f (l + 1 • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)

pp: case inr
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + 1 • a)) (f y)

Tactic:
;

Goal state after:
case inl
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
hny : y - 1 • a ∈ Ioc l (l + a)
hn : 1 ≤ 1
hy : R (f (l + 1 • a)) (f y)
⊢ R (f (l + 1 • a)) (f y)

case inr
F : Type u_1
G : Type u_2
H : Type u_3
inst✝⁷ : FunLike F G H
a : G
b : H
inst✝⁶ : AddCommGroup G
inst✝⁵ : LinearOrder G
inst✝⁴ : IsOrderedAddMonoid G
inst✝³ : Archimedean G
inst✝² : AddGroup H
inst✝¹ : AddConstMapClass F G H a b
f : F
R : H → H → Prop
inst✝ : IsTrans H R
ha : 0 < a
l : G
hf : ∀ x ∈ Icc l (l + a), ∀ y ∈ Icc l (l + a), x < y → R (f x) (f y)
hR : Covariant H H (fun x y ↦ y + x) R
ha' : 0 ≤ a
x y : G
hxy : x < y
hx : x ∈ Ico l (l + a)
n : ℤ
hny : y - n • a ∈ Ioc l (l + a)
hn✝ : 1 ≤ n
hy : R (f (l + n • a)) (f y)
hn : 1 < n
⊢ R (f (l + 1 • a)) (f y)
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 1 ≤ a

Tactic:
;

Goal state after:
case refine_3
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 ≤ a
⊢ 1 ≤ a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 2⁻¹ < a
⊢ ↑⌈(2 - 1)⁻¹⌉ / 2 < a

Tactic:
norm_num at ha ⊢

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 / 2 < a
⊢ 1 / 2 < a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
;

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 / 2 < a
⊢ 1 / 2 < a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 2⁻¹ ≤ a
⊢ ↑⌈(2 - 1)⁻¹⌉ / 2 ≤ a

Tactic:
norm_num at ha ⊢

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a

Tactic:
;

Goal state after:
k : Type u_4
inst✝³ : Field k
inst✝² : LinearOrder k
inst✝¹ : IsOrderedRing k
inst✝ : FloorRing k
a : k
ha : 1 / 2 ≤ a
⊢ 1 / 2 ≤ a
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mk
R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
H₂ : FloorRing R
floor✝ ceil✝ : R → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ } = H₂

Tactic:
;

Goal state after:
case mk
R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
H₂ : FloorRing R
floor✝ ceil✝ : R → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ } = H₂
Module: Mathlib.Algebra.Order.Floor.Ring

Goal state before:
pp: case mk.mk
R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
floor✝¹ ceil✝¹ : R → ℤ
gc_coe_floor✝¹ : GaloisConnection Int.cast floor✝¹
gc_ceil_coe✝¹ : GaloisConnection ceil✝¹ Int.cast
floor✝ ceil✝ : R → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝¹, ceil := ceil✝¹, gc_coe_floor := gc_coe_floor✝¹, gc_ceil_coe := gc_ceil_coe✝¹ } =
    { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ }

Tactic:
;

Goal state after:
case mk.mk
R : Type u_4
inst✝¹ : Ring R
inst✝ : LinearOrder R
floor✝¹ ceil✝¹ : R → ℤ
gc_coe_floor✝¹ : GaloisConnection Int.cast floor✝¹
gc_ceil_coe✝¹ : GaloisConnection ceil✝¹ Int.cast
floor✝ ceil✝ : R → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝¹, ceil := ceil✝¹, gc_coe_floor := gc_coe_floor✝¹, gc_ceil_coe := gc_ceil_coe✝¹ } =
    { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ }
Module: Mathlib.Algebra.Group.Action.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ g⁻¹ • h • x = x → g = h

Tactic:
← mul_smul,

Goal state after:
α : Type u_5
β : Type u_6
inst✝¹ : Group α
inst✝ : MulAction α β
H : ∀ (g : α) (x : β), g • x = x → g = 1
g h : α
x : β
⊢ (g⁻¹ * h) • x = x → g = h
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
inst✝ : AddMonoid G
a x✝ : G
⊢ (Multiplicative.toAdd 1 +ᵥ AddConstMap.id) x✝ = 1 x✝

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : AddMonoid G
a x✝ : G
⊢ (Multiplicative.toAdd 1 +ᵥ AddConstMap.id) x✝ = 1 x✝
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: G : Type u_1
inst✝ : AddMonoid G
a : G
x✝² x✝¹ : Multiplicative G
x✝ : G
⊢ (Multiplicative.toAdd (x✝² * x✝¹) +ᵥ AddConstMap.id) x✝ =
    ((Multiplicative.toAdd x✝² +ᵥ AddConstMap.id) * (Multiplicative.toAdd x✝¹ +ᵥ AddConstMap.id)) x✝

Tactic:
;

Goal state after:
G : Type u_1
inst✝ : AddMonoid G
a : G
x✝² x✝¹ : Multiplicative G
x✝ : G
⊢ (Multiplicative.toAdd (x✝² * x✝¹) +ᵥ AddConstMap.id) x✝ =
    ((Multiplicative.toAdd x✝² +ᵥ AddConstMap.id) * (Multiplicative.toAdd x✝¹ +ᵥ AddConstMap.id)) x✝
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
x✝ : ↑(Ico 0 1) → G
x : ↑(Ico 0 1)
⊢ (fun f x ↦ f ↑x) ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x✝) x = x✝ x

Tactic:
;

Goal state after:
R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
x✝ : ↑(Ico 0 1) → G
x : ↑(Ico 0 1)
⊢ (fun f x ↦ f ↑x) ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) x✝) x = x✝ x
Module: Mathlib.Algebra.AddConstMap.Basic

Goal state before:
pp: R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : R →+c[1, a] G
x : R
⊢ ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) ((fun f x ↦ f ↑x) f)) x = f x

Tactic:
;

Goal state after:
R : Type u_1
G : Type u_2
inst✝⁴ : Ring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : FloorRing R
inst✝ : AddGroup G
a : G
f : R →+c[1, a] G
x : R
⊢ ((fun f ↦ { toFun := fun x ↦ f ⟨Int.fract x, ⋯⟩ + ⌊x⌋ • a, map_add_const' := ⋯ }) ((fun f x ↦ f ↑x) f)) x = f x
Module: Mathlib.Algebra.Group.Pointwise.Set.Scalar

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x✝ : γ
⊢ x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t

Tactic:
;

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x✝ : γ
⊢ x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: case mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α)) l) (Quot.mk (⇑(isSetoid α)) l)

Tactic:
;

Goal state after:
case mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α)) l) (Quot.mk (⇑(isSetoid α)) l)
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: case mk.mk.mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
c✝ : Multiset α
l₃ : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₂) →
    Multiset.Le (Quot.mk (⇑(isSetoid α)) l₂) (Quot.mk (⇑(isSetoid α)) l₃) →
      Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₃)

Tactic:
;

Goal state after:
case mk.mk.mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
c✝ : Multiset α
l₃ : List α
⊢ Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₂) →
    Multiset.Le (Quot.mk (⇑(isSetoid α)) l₂) (Quot.mk (⇑(isSetoid α)) l₃) →
      Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₃)
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: case mk.mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
h₁ : Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₂)
h₂ : Multiset.Le (Quot.mk (⇑(isSetoid α)) l₂) (Quot.mk (⇑(isSetoid α)) l₁)
⊢ Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
β : Type v
γ : Type u_2
a✝ : Multiset α
l₁ : List α
b✝ : Multiset α
l₂ : List α
h₁ : Multiset.Le (Quot.mk (⇑(isSetoid α)) l₁) (Quot.mk (⇑(isSetoid α)) l₂)
h₂ : Multiset.Le (Quot.mk (⇑(isSetoid α)) l₂) (Quot.mk (⇑(isSetoid α)) l₁)
⊢ Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
H✝ : ∀ (a : α), a ∈ s₂ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H✝ =
    ↑(List.pmap f l₁ H₁)

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
s₂ : Multiset α
e : ↑l₁ = s₂
H✝ : ∀ (a : α), a ∈ s₂ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) e H✝ =
    ↑(List.pmap f l₁ H₁)
Module: Mathlib.Data.Multiset.Defs

Goal state before:
pp: α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
H✝ : ∀ (a : α), a ∈ ↑l₁ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) ⋯ H✝ =
    ↑(List.pmap f l₁ H₁)

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
γ : Type u_2
p : α → Prop
f : (a : α) → p a → β
s : Multiset α
l₁ l₂ : List α
pp : l₁ ~ l₂
H₂ : ∀ (a : α), a ∈ l₂ → p a
H₁ : ∀ (a : α), a ∈ l₁ → p a
H✝ : ∀ (a : α), a ∈ ↑l₁ → p a
⊢ Eq.ndrec (motive := fun s ↦ (∀ (a : α), a ∈ s → p a) → Multiset β) (fun x ↦ ↑(List.pmap f l₁ H₁)) ⋯ H✝ =
    ↑(List.pmap f l₁ H₁)
Module: Mathlib.Data.Finset.Defs

Goal state before:
pp: case refl
α : Type u_1
s : Multiset α
nodup✝¹ nodup✝ : s.Nodup
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }

Tactic:
;

Goal state after:
case refl
α : Type u_1
s : Multiset α
nodup✝¹ nodup✝ : s.Nodup
⊢ { val := s, nodup := nodup✝¹ } = { val := s, nodup := nodup✝ }
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) • p₃ = (p₃ /ₛ p₂) • p₁

Tactic:
rw [← @sdiv_eq_one_iff_eq G, smul_sdiv_assoc, sdiv_smul_eq_sdiv_div]

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
p₁ p₂ p₃ : P
⊢ (p₁ /ₛ p₂) * ((p₃ /ₛ p₁) / (p₃ /ₛ p₂)) = 1
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
s t : Set P
x✝ : G
⊢ x✝ ∈ v • s /ₛ v • t ↔ x✝ ∈ s /ₛ t

Tactic:
;

Goal state after:
G : Type u_1
P : Type u_2
inst✝¹ : CommGroup G
inst✝ : Torsor G P
v : G
s t : Set P
x✝ : G
⊢ x✝ ∈ v • s /ₛ v • t ↔ x✝ ∈ s /ₛ t
Module: Mathlib.Data.Multiset.Count

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ List.countP (fun b ↦ decide (a = b)) l = List.countP (fun x ↦ x == a) l

Tactic:
@eq_comm _ a

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
⊢ List.countP (fun b ↦ decide (b = a)) l = List.countP (fun x ↦ x == a) l
Module: Mathlib.Algebra.Torsor.Basic

Goal state before:
pp: G : Type u_5
inst✝ : AddCommGroup G
x x✝ : G
⊢ (pointReflection x) x✝ = (Equiv.subLeft (2 • x)) x✝

Tactic:
;

Goal state after:
G : Type u_5
inst✝ : AddCommGroup G
x x✝ : G
⊢ (pointReflection x) x✝ = (Equiv.subLeft (2 • x)) x✝
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mk.nil
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
⊢ Quot.mk ⇑(isSetoid α) [] = 0

pp: case mk.cons
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) (a :: l) = 0

Tactic:
;

Goal state after:
case mk.nil
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
⊢ Quot.mk ⇑(isSetoid α) [] = 0

case mk.cons
α : Type u_1
β : Type v
γ : Type u_2
inst✝ : IsEmpty α
a✝ : Multiset α
a : α
l : List α
⊢ Quot.mk (⇑(isSetoid α)) (a :: l) = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mk.mk
α : Type u_1
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk (⇑(isSetoid α)) l₁ = a ::ₘ Quot.mk (⇑(isSetoid α)) l₂ ↔
    Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
a : α
s✝ : Multiset α
l₁ : List α
t✝ : Multiset α
l₂ : List α
⊢ a ::ₘ Quot.mk (⇑(isSetoid α)) l₁ = a ::ₘ Quot.mk (⇑(isSetoid α)) l₂ ↔
    Quot.mk (⇑(isSetoid α)) l₁ = Quot.mk (⇑(isSetoid α)) l₂
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case mk
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk (⇑(isSetoid α)) l)

Tactic:
;

Goal state after:
case mk
α : Type u_1
p : Multiset α → Prop
empty : p 0
cons : ∀ (a : α) (s : Multiset α), p s → p (a ::ₘ s)
s✝ : Multiset α
l : List α
⊢ p (Quot.mk (⇑(isSetoid α)) l)
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case e_2
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x✝² x✝¹ : List α
h : x✝² ≈ x✝¹
a✝ : α
l✝ l'✝ : List α
b✝ : C ⟦l✝⟧
b'✝ : C ⟦l'✝⟧
hl : l✝ ~ l'✝
x✝ : b✝ ≍ b'✝
⊢ ⟦l✝⟧ = ⟦l'✝⟧

Tactic:
;

Goal state after:
case e_2
α : Type u_1
β : Type v
γ : Type u_2
C : Multiset α → Sort u_3
C_0 : C 0
C_cons : (a : α) → (m : Multiset α) → C m → C (a ::ₘ m)
C_cons_heq :
  ∀ (a a' : α) (m : Multiset α) (b : C m), C_cons a (a' ::ₘ m) (C_cons a' m b) ≍ C_cons a' (a ::ₘ m) (C_cons a m b)
m : Multiset α
x✝² x✝¹ : List α
h : x✝² ≈ x✝¹
a✝ : α
l✝ l'✝ : List α
b✝ : C ⟦l✝⟧
b'✝ : C ⟦l'✝⟧
hl : l✝ ~ l'✝
x✝ : b✝ ≍ b'✝
⊢ ⟦l✝⟧ = ⟦l'✝⟧
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0

Tactic:
;

Goal state after:
α : Type u_1
s : Multiset α
l : List α
H : ∀ (x : α), ¬x ∈ Quot.mk (⇑(isSetoid α)) l
⊢ Quot.mk ⇑(isSetoid α) [] = 0
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
h₁ : a ∈ t
h₂ : s ≤ t
⊢ a ::ₘ s ≤ t

Tactic:
;

Goal state after:
α : Type u_1
s t : Multiset α
a : α
hs : ¬a ∈ s
h₁ : a ∈ t
h₂ : s ≤ t
⊢ a ::ₘ s ≤ t
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup

pp: case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
h : ∀ (a : α), ¬[a, a] <+ head✝ :: tail✝
⊢ (head✝ :: tail✝).Nodup

Tactic:
;

Goal state after:
case nil
α : Type u
h : ∀ (a : α), ¬[a, a] <+ []
⊢ [].Nodup

case cons
α : Type u
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a : α), ¬[a, a] <+ tail✝) → tail✝.Nodup
h : ∀ (a : α), ¬[a, a] <+ head✝ :: tail✝
⊢ (head✝ :: tail✝).Nodup
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
b : Multiset β
⊢ (0 = 0 ∧ b = 0 ∨ ∃ a b_1 as bs, r a b_1 ∧ Rel r as bs ∧ 0 = a ::ₘ as ∧ b = b_1 ::ₘ bs) ↔ b = 0
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
j : Fin l.length
i : ℕ
hi : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) j
⊢ ⟨i, hi⟩ = j

Tactic:
;

Goal state after:
α : Type u
l : List α
h : ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]
j : Fin l.length
i : ℕ
hi : i < l.length
hg : (fun i ↦ l[↑i]) ⟨i, hi⟩ = (fun i ↦ l[↑i]) j
⊢ ⟨i, hi⟩ = j
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨ ∃ a_1 b as bs, r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔ a = 0

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
a : Multiset α
⊢ (a = 0 ∧ 0 = 0 ∨ ∃ a_1 b as bs, r a_1 b ∧ Rel r as bs ∧ a = a_1 ::ₘ as ∧ 0 = b ::ₘ bs) ↔ a = 0
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
a : α
h : ¬a ∈ s
⊢ s ≤ a ::ₘ s
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
h : a ::ₘ s.erase a ≤ a ::ₘ t
m : a ∈ s
⊢ s.erase a ≤ t
Module: Mathlib.Data.Multiset.ZeroCons

Goal state before:
pp: case cons.inl
α : Type u_1
β : Type v
r : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
x : α
y : β
s : Multiset α
t : Multiset β
hxy : r x y
a✝ : Rel r s t
ih : ∀ {a : α}, a ∈ s → ∃ b, b ∈ t ∧ r a b
a : α
ha✝ : a ∈ x ::ₘ s
ha : a = x
⊢ ∃ b, b ∈ y ::ₘ t ∧ r a b

Tactic:
exact ⟨y, mem_cons_self _ _, ha.symm ▸ hxy⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
a : α
⊢ count a (s + t - u) = count a (s + (t - u))

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
hut : u ≤ t
a : α
⊢ count a (s + t - u) = count a (s + (t - u))
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ 0 < count x l → count x l = 1

Tactic:
;

Goal state after:
α : Type u
l : List α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x : α
⊢ count x l ≤ 1 ↔ 0 < count x l → count x l = 1
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
a✝ : α
⊢ count a✝ (s - (t + u)) = count a✝ (s - t - u)

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
a✝ : α
⊢ count a✝ (s - (t + u)) = count a✝ (s - t - u)
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ count a (s + t - t) = count a s

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a : α
⊢ count a (s + t - t) = count a s
Module: Mathlib.Data.Multiset.AddSub

Goal state before:
pp: α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
r : α → β → Prop
as : Multiset α
bs₀ bs₁ : Multiset β
⊢ (∃ bs₀_1 bs₁_1, Rel (flip r) bs₀ bs₀_1 ∧ Rel (flip r) bs₁ bs₁_1 ∧ as = bs₀_1 + bs₁_1) ↔
    ∃ as₀ as₁, Rel r as₀ bs₀ ∧ Rel r as₁ bs₁ ∧ as = as₀ + as₁
Module: Mathlib.Data.Finset.Attach

Goal state before:
pp: α : Type u_1
s : Finset α
x✝ : ↥s
⊢ x✝ ∈ ↑s.attach ↔ x✝ ∈ Set.univ

Tactic:
;

Goal state after:
α : Type u_1
s : Finset α
x✝ : ↥s
⊢ x✝ ∈ ↑s.attach ↔ x✝ ∈ Set.univ
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a

Tactic:
;

Goal state after:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α) (b : β), b ∈ f a → b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : f a = some b
b' : β
bm' : f a' = some b'
e : b = b'
⊢ b ∈ f a
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup

Tactic:
;

Goal state after:
α : Type u
l : List α
a : α
h : ¬a ∈ l
h' : l.Nodup
⊢ (l ++ [a]).Nodup
Module: Mathlib.Data.Multiset.MapFold

Goal state before:
pp: α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ map f m ≍ map f' m

Tactic:
;

Goal state after:
α : Type u_1
β : Type v
m : Multiset α
f f' : α → β
hf : ∀ (a : α), a ∈ m → f a ≍ f' a
⊢ map f m ≍ map f' m
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup

Tactic:
;

Goal state after:
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : a ∈ l
⊢ l.Nodup
Module: Mathlib.Data.List.Nodup

Goal state before:
pp: α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ ¬a ∈ l ∧ l.Nodup

Tactic:
;

Goal state after:
α : Type u
l : List α
a : α
inst✝¹ : BEq α
inst✝ : LawfulBEq α
h : l.Nodup
h' : ¬a ∈ l
⊢ ¬a ∈ l ∧ l.Nodup