mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (a : α), p a ↔ q (e a)
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
h : n ≤ m
⊢ f^[m - n + ?m.30] a = f^[?m.30] a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : α ≃ β
h : ∀ (b : β), p (e.symm b) ↔ q b
⊢ (∃! b, p (e.symm b)) ↔ ∃! b, q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
a : α
hf : Injective f
ha : f^[m] a = f^[n] a
⊢ f^[m - n] a = a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
p : α → Prop
q : β → Prop
e : { a // p a } ≃ { b // q b }
⊢ (∃! a, p a) ↔ ∃! b, q b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
p : α → Prop
q : β → Prop
e x✝ : α ≃ β
⊢ (fun f ↦ ofBijective ↑f ⋯) ((fun f ↦ ⟨⇑f, ⋯⟩) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
⊢ LeftInverse (Quot.map ⇑e.symm ⋯) (Quot.map ⇑e ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: case mk
α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
x✝ : Quot rb
a : β
⊢ Quot.map ⇑e ⋯ (Quot.map ⇑e.symm ⋯ (mk rb a)) = mk rb a

Tactic:
simp only [Quot.map, Equiv.apply_symm_apply]

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
ra : α → α → Prop
rb : β → β → Prop
e : α ≃ β
eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)
⊢ RightInverse (Quot.map ⇑e.symm ⋯) (Quot.map ⇑e ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
r : α → α → Prop
e : α ≃ β
x✝¹ x✝ : α
⊢ r x✝¹ x✝ ↔ r (e.symm (e x✝¹)) (e.symm (e x✝))

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
i : Fin 2
⊢ (fun b ↦ bif b then 1 else 0) ((fun i ↦ i == 1) i) = i

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
b : Bool
⊢ (fun i ↦ i == 1) ((fun b ↦ bif b then 1 else 0) b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : α → α
a : α
l : List β
⊢ foldl (fun b x ↦ f b) a l = f^[l.length] a

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
β : Type v
f : β → β
b : β
a : α
l : List α
⊢ foldr (fun x ↦ f) b (a :: l) = f^[(a :: l).length] b

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
f : (i : ι) → α i → α i
n : ℕ
⊢ (Pi.map f)^[n] = Pi.map fun i ↦ (f i)^[n]

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsRightCancelMul R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsLeftCancelMul R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
⊢ FaithfulSMul R A ↔ Injective fun r ↦ r • 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ FaithfulSMul G α ↔ ∀ (g : G), (∀ (a : α), g • a = a) → g = 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
inst✝⁸ : Monoid S
inst✝⁷ : MulOneClass T
inst✝⁶ : SMul R S
inst✝⁵ : SMul R T
inst✝⁴ : MulAction S T
inst✝³ : IsScalarTower R S S
inst✝² : IsScalarTower R T T
inst✝¹ : IsScalarTower R S T
inst✝ : FaithfulSMul R T
⊢ FaithfulSMul R S

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
inst✝¹⁰ : Monoid S
inst✝⁹ : MulOneClass T
inst✝⁸ : SMul R S
inst✝⁷ : IsScalarTower R S S
inst✝⁶ : MulAction S T
inst✝⁵ : IsScalarTower S T T
inst✝⁴ : SMul R T
inst✝³ : IsScalarTower R T T
inst✝² : IsScalarTower R S T
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S T
⊢ FaithfulSMul R T

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_4
N : Type u_5
P : Type u_6
Q : Type u_7
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul N P
inst✝⁵ : SMul N Q
inst✝⁴ : SMul P Q
inst✝³ : FaithfulSMul P Q
inst✝² : IsScalarTower M N Q
inst✝¹ : IsScalarTower M P Q
inst✝ : IsScalarTower N P Q
m : M
n : N
p : P
⊢ (m • n) • p = m • n • p

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
inst✝¹ : (i : ι) → One (M i)
inst✝ : DecidableEq ι
i : ι
x : M i
⊢ mulSingle i x = 1 ↔ x = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
inst✝² : (i : ι) → One (M i)
inst✝¹ : (i : ι) → One (N i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i
hf' : ∀ (i : ι), f' i 1 = 1
i : ι
x : M i
j : ι
⊢ f' j (mulSingle i x j) = mulSingle i (f' i x) j

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
O : ι → Type u_8
inst✝³ : (i : ι) → One (M i)
inst✝² : (i : ι) → One (N i)
inst✝¹ : (i : ι) → One (O i)
inst✝ : DecidableEq ι
f' : (i : ι) → M i → N i → O i
hf' : ∀ (i : ι), f' i 1 1 = 1
i : ι
x : M i
y : N i
j : ι
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : DecidableEq ι
M : Type u_9
inst✝ : One M
i : ι
x : M
j : ι
⊢ mulSingle i x j = mulSingle j x i

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N β
f : α → β
hf : Injective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ f (c₁ • c₂ • x) = f (c₂ • c₁ • x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul M β
inst✝¹ : SMul N β
inst✝ : SMulCommClass M N α
f : α → β
hf : Surjective f
h₁ : ∀ (c : M) (x : α), f (c • x) = c • f x
h₂ : ∀ (c : N) (x : α), f (c • x) = c • f x
c₁ : M
c₂ : N
x : α
⊢ c₁ • c₂ • f x = c₂ • c₁ • f x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α✝ : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
M : Type u_9
α : Type u_10
inst✝¹ : CommMonoid M
inst✝ : MulAction M α
a a' : M
b : α
⊢ a • a' • b = a' • a • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
α : Type u_10
inst✝² : SMul M α
inst✝¹ : SMul Mᵐᵒᵖ α
inst✝ : IsCentralScalar M α
m : Mᵐᵒᵖ
a : α
⊢ MulOpposite.unop m • a = m • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul Mᵐᵒᵖ α
inst✝² : IsCentralScalar M α
inst✝¹ : SMul N α
inst✝ : SMulCommClass M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ m • n • a = n • m • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : SMul M α
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : SMulCommClass M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ m • n • a = n • m • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul M α
inst✝⁶ : SMul Mᵐᵒᵖ α
inst✝⁵ : IsCentralScalar M α
inst✝⁴ : SMul M N
inst✝³ : SMul Mᵐᵒᵖ N
inst✝² : IsCentralScalar M N
inst✝¹ : SMul N α
inst✝ : IsScalarTower M N α
m : Mᵐᵒᵖ
n : N
a : α
⊢ (m • n) • a = m • n • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁵ : SMul M α
inst✝⁴ : SMul M N
inst✝³ : SMul N α
inst✝² : SMul Nᵐᵒᵖ α
inst✝¹ : IsCentralScalar N α
inst✝ : IsScalarTower M N α
m : M
n : Nᵐᵒᵖ
a : α
⊢ (m • n) • a = m • n • a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
⊢ Sort ?u.25

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝² : DivInvMonoid β
inst✝¹ : SMul α β
inst✝ : IsScalarTower α β β
r : α
x y : β
⊢ r • x / y = r • (x / y)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁷ : SMul α β
inst✝⁶ : SMul α γ
inst✝⁵ : SMul β δ
inst✝⁴ : SMul α δ
inst✝³ : SMul γ δ
inst✝² : IsScalarTower α β δ
inst✝¹ : IsScalarTower α γ δ
inst✝ : SMulCommClass β γ δ
a : α
b : β
c : γ
d : δ
⊢ (a • b) • c • d = (a • c) • b • d

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝⁵ : Mul α
inst✝⁴ : Mul β
inst✝³ : SMul α β
inst✝² : IsScalarTower α β β
inst✝¹ : IsScalarTower α α β
inst✝ : SMulCommClass α β β
a : α
b : β
c : α
d : β
⊢ a • b * c • d = (a * c) • (b * d)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
⊢ ¬(x.isLeft = true ∧ x.isRight = true)

Tactic:
by

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
f : α → γ
g : β → γ
⊢ Sum.elim f g ∘ swap = Sum.elim g f

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : α ⊕ β → Sort u_3
p : ((ab : α ⊕ β) → γ ab) → Prop
⊢ (∃ fab, p fab) ↔ ∃ fa fb, p fun t ↦ rec fa fb t

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy x (r • a) (r • b)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
P : α ⊕ β → Sort u_3
f : (i : α) → P (inl i)
g : (i : β) → P (inr i)
x y : α ⊕ β
h : x = y
⊢ rec f g x = cast ⋯ (rec f g y)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
a : α
⊢ x = inl a ↔ ∃ h, x.getLeft h = a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
b : β
⊢ x = inr b ↔ ∃ h, x.getRight h = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝³ : SMul M α
inst✝² : Mul α
inst✝¹ : SMulCommClass M α α
inst✝ : IsScalarTower M α α
x a b : α
h : SemiconjBy x a b
r : M
⊢ SemiconjBy (r • x) a b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isLeft = true
h₂ : x.getLeft?.isSome = true
⊢ x.getLeft h₁ = x.getLeft?.get h₂

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
h₁ : x.isRight = true
h₂ : x.getRight?.isSome = true
⊢ x.getRight h₁ = x.getRight?.get h₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
⊢ (fun x ↦ a • x)^[0] = fun x ↦ a ^ 0 • x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
⊢ x.getLeft?.isSome = true ↔ x.isLeft = true

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
x : α ⊕ β
⊢ x.getRight?.isSome = true ↔ x.isRight = true

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ x = Sum.elim (update f i x) g (inl i)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : α
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inl i → Sum.elim f g x_1 = Sum.elim (update f i x) g x_1

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ x = Sum.elim f (update g i x) (inr i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
⊢ (fun x ↦ a • x)^[n + 1] = fun x ↦ a ^ (n + 1) • x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α → γ
g : β → γ
i : β
x : γ
⊢ ∀ (x_1 : α ⊕ β), x_1 ≠ inr i → Sum.elim f g x_1 = Sum.elim f (update g i x) x_1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
α : Type u_5
inst✝¹ : Monoid M
inst✝ : MulAction M α
a : M
n : ℕ
x : α
⊢ (fun x ↦ a • x)^[n] x = a ^ n • x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq α
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : α
x : γ
⊢ update f (inl i) x (inl j) = update (f ∘ inl) i x j

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update (f ∘ inr) i x j

Tactic:
← update_inr_comp_inr,

Goal state after:
α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = (update f (inr i) x ∘ inr) j
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : M
inst✝ : SMul M β
f : β → α
hf : Injective f
smul : ∀ (c : M) (x : β), f (c • x) = c • f x
c₁ c₂ : M
x : β
⊢ f ((c₁ * c₂) • x) = f (c₁ • c₂ • x)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : M
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
⊢ ∀ (x y : M) (b : β), (x * y) • b = x • y • b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝² : Monoid M
inst✝¹ : MulAction M α
a : M
inst✝ : SMul M β
f : α → β
hf : Surjective f
smul : ∀ (c : M) (x : α), f (c • x) = c • f x
⊢ ∀ (b : β), 1 • b = b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
inst✝¹ : DecidableEq β
inst✝ : DecidableEq (α ⊕ β)
f : α ⊕ β → γ
i j : β
x : γ
⊢ update f (inr i) x (inr j) = update (f ∘ inr) i x j

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isLeft = true ↔ y.isLeft = true

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝⁴ : Monoid M✝
inst✝³ : MulAction M✝ α
a : M✝
R : Type u_9
M : Type u_10
inst✝² : CommMonoid M
inst✝¹ : SMul R M
inst✝ : IsScalarTower R M M
r : R
s x : M
⊢ r • s • x = s • r • x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h : LiftRel r s x y
⊢ x.isRight = true ↔ y.isRight = true

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
⊢ (r • x) ^ 0 = r ^ 0 • x ^ 0

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
c : γ
h : LiftRel r s x (inl c)
⊢ x.isLeft = true

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
a : α
h : LiftRel r s (inl a) y
⊢ y.isLeft = true

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M N
inst✝¹ : IsScalarTower M N N
inst✝ : SMulCommClass M N N
r : M
x : N
n : ℕ
⊢ (r • x) ^ (n + 1) = r ^ (n + 1) • x ^ (n + 1)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
d : δ
h : LiftRel r s x (inr d)
⊢ x.isRight = true

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ g⁻¹ • g • a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a : α
⊢ g • g⁻¹ • a = a

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
y : γ ⊕ δ
b : β
h : LiftRel r s (inr b) y
⊢ y.isRight = true

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g⁻¹ • a = b
⊢ a = g • b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isLeft = true
⊢ ∃ a c, r a c ∧ x = inl a ∧ y = inl c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g • b
⊢ g⁻¹ • a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ g • a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : g • a = b
⊢ a = g⁻¹ • b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
x : α ⊕ β
y : γ ⊕ δ
h₁ : LiftRel r s x y
h₂ : x.isRight = true
⊢ ∃ b d, s b d ∧ x = inr b ∧ y = inr d

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy x (r • a) (r • b)
⊢ SemiconjBy x a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy (r • x) a b
⊢ SemiconjBy x a b

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Sort u_3
f : α → γ
g₁ g₂ : β → γ
hg : Sum.elim f g₁ = Sum.elim f g₂
b : β
⊢ g₁ b = g₂ b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
⊢ g • a * g⁻¹ • a⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Group H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
g : G
a : H
n : ℤ
⊢ (g • a) ^ n = g ^ n • a ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
d : δ
⊢ ∃ a, g a = d

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: A : Type u_9
B : Type u_10
G : Type u_11
inst✝⁴ : CommMonoid G
inst✝³ : SMul A G
inst✝² : SMul B G
inst✝¹ : IsScalarTower A G G
inst✝ : IsScalarTower B G G
r : A
s : B
x : G
⊢ r • s • x = s • r • x

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: R₁ : Type u_9
R : Type u_10
inst✝³ : Monoid R₁
inst✝² : CommMonoid R
inst✝¹ : MulAction R₁ R
inst✝ : SMulCommClass R₁ R R
x₁ : R₁
y z : R
⊢ (x₁ • y) • z = x₁ • y • z

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: α : Type u_5
M : Type u_9
N : Type u_10
inst✝⁴ : Monoid N
inst✝³ : SMul M N
inst✝² : MulAction N α
inst✝¹ : SMul M α
inst✝ : IsScalarTower M N α
x : M
y : α
⊢ (x • 1) • y = x • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
inst✝² : MulOneClass N
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N N
x : M
y : N
⊢ x • 1 * y = x • y

Tactic:
by

Goal state after: