awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Defs
Goal:
R : Type u_1
M : Type u_2
G : Type u_3
inst : AddGroup G
inst_1 : IsAddTorsionFree G
n : ℤ
x : G
hx : n ≠ 0 ∧ x ≠ 0
⊢ n • x ≠ 0

Tactic:
simpa using (zsmul_right_injective hx.1).ne hx.2

Premises used: Function.Injective.ne, And.right, And.left, zsmul_right_injective
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Pi
Goal:
I : Type u
f : I → Type v
α : Type u_1
inst : Semiring α
inst_1 : IsDomain α
inst_2 : (i : I) → AddCommGroup (f i)
inst_3 : (i : I) → Module.{u_1, v} α (f i)
inst_4 : ∀ (i : I), NoZeroSMulDivisors.{u_1, v} α (f i)
⊢ NoZeroSMulDivisors α ((i : I) → f i)

Tactic:
⟨fun {_ _} h =>
    or_iff_not_imp_left.mpr fun hc =>
      funext fun i => (smul_eq_zero.mp (congr_fun h i)).resolve_left hc⟩

Premises used: Iff.mpr, Or.resolve_left, NoZeroSMulDivisors.mk, funext, Classical.or_iff_not_imp_left, Iff.mp, congr_fun, smul_eq_zero
-- Module: Mathlib.Algebra.NoZeroSMulDivisors.Pi
Goal:
I : Type u
f : I → Type v
ι : Type u_1
α : Type u_2
β : Type u_3
inst : Semiring α
inst_1 : IsDomain α
inst_2 : AddCommGroup β
inst_3 : Module α β
inst_4 : NoZeroSMulDivisors α β
⊢ NoZeroSMulDivisors α (ι → β)

Tactic:
Pi.noZeroSMulDivisors _

Premises used: Pi.noZeroSMulDivisors
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
simp : x * z + y * z - (z * x + z * y) = x * z - z * x + (y * z - z * y)
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

Tactic:
simp only [Ring.lie_def, mul_add, add_mul]

Premises used: add_mul, Ring.lie_def, mul_add
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
⊢ x * z + y * z - (z * x + z * y) = x * z - z * x + (y * z - z * y)

Tactic:
abel
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
simp : x * y + x * z - (y * x + z * x) = x * y - y * x + (x * z - z * x)
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

Tactic:
simp only [Ring.lie_def, mul_add, add_mul]

Premises used: add_mul, Ring.lie_def, mul_add
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
⊢ x * y + x * z - (y * x + z * x) = x * y - y * x + (x * z - z * x)

Tactic:
abel
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
⊢ ∀ (x : L), ⁅x, x⁆ = 0

Tactic:
simp [Ring.lie_def]

Premises used: Ring.lie_def
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
have := LieAdmissibleRing.assoc_def x y z
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
x y z : L
this :
  x * y * z - x * (y * z) + (z * x * y - z * (x * y)) + (y * z * x - y * (z * x)) =
    y * x * z - y * (x * z) + (z * y * x - z * (y * x)) + (x * z * y - x * (z * y))
⊢ ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆

Tactic:
grind [Ring.lie_def, mul_sub, sub_mul]

Premises used: mul_sub, sub_mul, Ring.lie_def
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieAdmissibleRing L
inst_2 : LieAdmissibleAlgebra R L
r : R
x y : L
⊢ ⁅x, r • y⁆ = r • ⁅x, y⁆

Tactic:
simp [Ring.lie_def, mul_smul_comm, smul_mul_assoc, ← smul_sub]

Premises used: smul_mul_assoc, smul_sub, Ring.lie_def, mul_smul_comm
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : L
⊢ associator x y z = associator y x z

Tactic:
have assoc_xyz := LeftPreLieRing.assoc_symm' x y z
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator y x z
⊢ associator z x y = associator x z y

Tactic:
have assoc_zxy := LeftPreLieRing.assoc_symm' z x y
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator y x z
assoc_zxy : associator z x y = associator x z y
⊢ associator y z x = associator z y x

Tactic:
have assoc_yzx := LeftPreLieRing.assoc_symm' y z x
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator y x z
assoc_zxy : associator z x y = associator x z y
assoc_yzx : associator y z x = associator z y x
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
grind
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : L
⊢ associator x y z = associator x z y

Tactic:
have assoc_xyz := RightPreLieRing.assoc_symm' x y z
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator x z y
⊢ associator z x y = associator z y x

Tactic:
have assoc_zxy := RightPreLieRing.assoc_symm' z x y
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator x z y
assoc_zxy : associator z x y = associator z y x
⊢ associator y z x = associator y x z

Tactic:
have assoc_yzx := RightPreLieRing.assoc_symm' y z x
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : L
assoc_xyz : associator x y z = associator x z y
assoc_zxy : associator z x y = associator z y x
assoc_yzx : associator y z x = associator y x z
⊢ associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
grind
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : Ring L
this : ∀ (a b c : L), associator a b c = 0
⊢ ∀ (x y z : L),
    associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
simp
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : Ring L
suffices : ∀ (a b c : L), associator a b c = 0
⊢ ∀ (x y z : L),
    associator x y z + associator z x y + associator y z x = associator y x z + associator z y x + associator x z y

Tactic:
suffices ∀ a b c : L, associator a b c = 0 by simp
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : Ring L
⊢ ∀ (a b c : L), associator a b c = 0

Tactic:
simp
-- Module: Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : Ring L
inst_2 : Algebra R L
⊢ ∀ (m : R) (n a : L), m • n • a = n • m • a

Tactic:
simp
-- Module: Mathlib.Algebra.NonAssoc.PreLie.Basic
Goal:
L : Type u_2
inst : LeftPreLieRing L
x y z : L
⊢ associator x y z = associator y x z

Tactic:
LeftPreLieRing.assoc_symm' x y z

Premises used: LeftPreLieRing.assoc_symm'
-- Module: Mathlib.Algebra.NonAssoc.PreLie.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LeftPreLieRing L
x y z : Lᵐᵒᵖ
⊢ associator x y z = associator x z y

Tactic:
simp [assoc_symm]

Premises used: LeftPreLieRing.assoc_symm
-- Module: Mathlib.Algebra.NonAssoc.PreLie.Basic
Goal:
L : Type u_2
inst : RightPreLieRing L
x y z : L
⊢ associator x y z = associator x z y

Tactic:
RightPreLieRing.assoc_symm' x y z

Premises used: RightPreLieRing.assoc_symm'
-- Module: Mathlib.Algebra.NonAssoc.PreLie.Basic
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : RightPreLieRing L
x y z : Lᵐᵒᵖ
⊢ associator x y z = associator y x z

Tactic:
simp [assoc_symm]

Premises used: RightPreLieRing.assoc_symm
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : α
b : P → α
c : ¬P → α
isTrue : ∀ (h : P), a * b h = a * b h
isFalse : ∀ (h : ¬P), a * c h = a * c h
⊢ (a * if h : P then b h else c h) = if h : P then a * b h else a * c h

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : α
b : P → α
c : ¬P → α
h : P
⊢ a * b h = a * b h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : α
b : P → α
c : ¬P → α
h : ¬P
⊢ a * c h = a * c h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a b c : α
⊢ (a * if P then b else c) = if P then a * b else a * c

Tactic:
mul_dite ..

Premises used: mul_dite, ite
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : α
isTrue : ∀ (h : P), a h * c = a h * c
isFalse : ∀ (h : ¬P), b h * c = b h * c
⊢ (if h : P then a h else b h) * c = if h : P then a h * c else b h * c

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : α
h : P
⊢ a h * c = a h * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : α
h : ¬P
⊢ b h * c = b h * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a b c : α
⊢ (if P then a else b) * c = if P then a * c else b * c

Tactic:
dite_mul ..

Premises used: dite_mul, ite
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
isTrue : ∀ (h : P), a h * c h = a h * c h
isFalse : ∀ (h : ¬P), b h * d h = b h * d h
⊢ HMul.hMul (α := α) (if h : P then a h else b h) (if h : P then c h else d h) = if h : P then a h * c h else b h * d h

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h : P
⊢ a h * c h = a h * c h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h : ¬P
⊢ b h * d h = b h * d h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a b c d : α
isTrue : P → a * c = a * c
isFalse : ¬P → b * d = b * d
⊢ ((if P then a else b) * if P then c else d) = if P then a * c else b * d

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a b c d : α
h : P
⊢ a * c = a * c

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Mul α
a b c d : α
h : ¬P
⊢ b * d = b * d

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : α
b : P → α
c : ¬P → α
isTrue : ∀ (h : P), a / b h = a / b h
isFalse : ∀ (h : ¬P), a / c h = a / c h
⊢ (a / if h : P then b h else c h) = if h : P then a / b h else a / c h

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : α
b : P → α
c : ¬P → α
h : P
⊢ a / b h = a / b h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : α
b : P → α
c : ¬P → α
h : ¬P
⊢ a / c h = a / c h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a b c : α
⊢ (a / if P then b else c) = if P then a / b else a / c

Tactic:
div_dite ..

Premises used: div_dite, ite
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : α
isTrue : ∀ (h : P), a h / c = a h / c
isFalse : ∀ (h : ¬P), b h / c = b h / c
⊢ (if h : P then a h else b h) / c = if h : P then a h / c else b h / c

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : α
h : P
⊢ a h / c = a h / c

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : α
h : ¬P
⊢ b h / c = b h / c

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a b c : α
⊢ (if P then a else b) / c = if P then a / c else b / c

Tactic:
dite_div ..

Premises used: dite_div, ite
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
isTrue : ∀ (h : P), a h / c h = a h / c h
isFalse : ∀ (h : ¬P), b h / d h = b h / d h
⊢ HDiv.hDiv (α := α) (if h : P then a h else b h) (if h : P then c h else d h) = if h : P then a h / c h else b h / d h

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h : P
⊢ a h / c h = a h / c h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h : ¬P
⊢ b h / d h = b h / d h

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u_2
P : Prop
inst : Decidable P
inst_1 : Div α
a b c d : α
⊢ ((if P then a else b) / if P then c else d) = if P then a / c else b / d

Tactic:
dite_div_dite ..

Premises used: dite_div_dite, ite
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
G : Type u_1
α : Type u
inst : One α
⊢ Nonempty α

Tactic:
⟨1⟩

Premises used: Nonempty.intro, OfNat.ofNat
-- Module: Mathlib.Algebra.Notation.Defs
Goal:
α : Type u
inst : One α
inst_1 : Subsingleton α
a : α
⊢ a = 1

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.Algebra.Notation.FiniteSupport
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : One γ
f : α × β → γ
a : α
h : HasFiniteMulSupport f
⊢ HasFiniteMulSupport.{u_2, u_3} (M := γ) fun (b : β) ↦ f (a, b)

Tactic:
(h.image Prod.snd).subset (mulSupport_along_fiber_subset f a)

Premises used: Set.Finite.subset, Set.Finite.image, Function.mulSupport_along_fiber_subset, Function.HasFiniteMulSupport, Prod.snd
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
isTrue : ∀ (h : p), 1 ≤ a h
isFalse : ∀ (h : ¬p), 1 ≤ b h
⊢ 1 ≤ dite p a b

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h : p
⊢ 1 ≤ a h

Tactic:
ha ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h : ¬p
⊢ 1 ≤ b h

Tactic:
hb ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), 1 ≤ a h
hb : ∀ (h : ¬p), 1 ≤ b h
h : p
⊢ 1 ≤ a h

Tactic:
exacts [ha ‹_›, hb ‹_›]
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
isTrue : ∀ (h : p), a h ≤ 1
isFalse : ∀ (h : ¬p), b h ≤ 1
⊢ dite p a b ≤ 1

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h : p
⊢ a h ≤ 1

Tactic:
ha ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h : ¬p
⊢ b h ≤ 1

Tactic:
hb ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LE α
ha : ∀ (h : p), a h ≤ 1
hb : ∀ (h : ¬p), b h ≤ 1
h : p
⊢ a h ≤ 1

Tactic:
exacts [ha ‹_›, hb ‹_›]
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
isTrue : ∀ (h : p), 1 < a h
isFalse : ∀ (h : ¬p), 1 < b h
⊢ 1 < dite p a b

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h : p
⊢ 1 < a h

Tactic:
ha ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h : ¬p
⊢ 1 < b h

Tactic:
hb ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), 1 < a h
hb : ∀ (h : ¬p), 1 < b h
h : p
⊢ 1 < a h

Tactic:
exacts [ha ‹_›, hb ‹_›]
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
isTrue : ∀ (h : p), a h < 1
isFalse : ∀ (h : ¬p), b h < 1
⊢ dite p a b < 1

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h : p
⊢ a h < 1

Tactic:
ha ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h : ¬p
⊢ b h < 1

Tactic:
hb ‹_›
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a : p → α
b : ¬p → α
inst_2 : LT α
ha : ∀ (h : p), a h < 1
hb : ∀ (h : ¬p), b h < 1
h : p
⊢ a h < 1

Tactic:
exacts [ha ‹_›, hb ‹_›]
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 1 ≤ a
hb : 1 ≤ b
isTrue : p → 1 ≤ a
isFalse : ¬p → 1 ≤ b
⊢ 1 ≤ if p then a else b

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h : p
⊢ 1 ≤ a

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : 1 ≤ a
hb : 1 ≤ b
h : ¬p
⊢ 1 ≤ b

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : a ≤ 1
hb : b ≤ 1
isTrue : p → a ≤ 1
isFalse : ¬p → b ≤ 1
⊢ (if p then a else b) ≤ 1

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : a ≤ 1
hb : b ≤ 1
h : p
⊢ a ≤ 1

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LE α
ha : a ≤ 1
hb : b ≤ 1
h : ¬p
⊢ b ≤ 1

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 1 < a
hb : 1 < b
isTrue : p → 1 < a
isFalse : ¬p → 1 < b
⊢ 1 < if p then a else b

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 1 < a
hb : 1 < b
h : p
⊢ 1 < a

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : 1 < a
hb : 1 < b
h : ¬p
⊢ 1 < b

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : a < 1
hb : b < 1
isTrue : p → a < 1
isFalse : ¬p → b < 1
⊢ (if p then a else b) < 1

Tactic:
split
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : a < 1
hb : b < 1
h : p
⊢ a < 1

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Lemmas
Goal:
α : Type u_1
inst : One α
p : Prop
inst_1 : Decidable p
a b : α
inst_2 : LT α
ha : a < 1
hb : b < 1
h : ¬p
⊢ b < 1

Tactic:
assumption
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
⊢ mulSingle (M := M) i x i = x

Tactic:
Function.update_self i x _

Premises used: Function.update_self, Pi.mulSingle
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i i' : ι
h : i' ≠ i
x : M i
⊢ mulSingle (M := M) i x i' = 1

Tactic:
Function.update_of_ne h x _

Premises used: Pi.mulSingle, Function.update_of_ne
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i i' : ι
h : i ≠ i'
x : M i
⊢ mulSingle (M := M) i x i' = 1

Tactic:
mulSingle_eq_of_ne h.symm x

Premises used: Ne.symm, Pi.mulSingle_eq_of_ne
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
⊢ Eq (α := (j : ι) → M j) (mulSingle (M := M) i 1) 1

Tactic:
Function.update_eq_self _ _

Premises used: Function.update_eq_self, Pi.mulSingle
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
⊢ mulSingle (M := M) i x = 1 ↔ x = 1

Tactic:
⟨fun h => ?_, fun h => h.symm ▸ mulSingle_one i⟩

Premises used: Pi.mulSingle_one, Eq.rec, Iff.intro, Eq.symm
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
refine : ∀ (h : mulSingle (M := M) i x = 1), x = 1
⊢ mulSingle (M := M) i x = 1 ↔ x = 1

Tactic:
refine ⟨fun h => ?_, fun h => h.symm ▸ mulSingle_one i⟩
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
h : mulSingle (M := M) i x = 1
rw : mulSingle (M := M) i x i = 1
rw₁ : Eq.{u_6 + 1} (α := M i) (1 i) 1
rw₂ rw₃ : Eq.{u_6 + 1} (α := M i) 1 1
⊢ x = 1

Tactic:
rw [← mulSingle_eq_same i x, h, one_apply]

Premises used: Pi.mulSingle_eq_same, Pi.one_apply
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
inst : (i : ι) → One (M i)
inst_1 : DecidableEq ι
i : ι
x : M i
⊢ mulSingle (M := M) i x ≠ 1 ↔ x ≠ 1

Tactic:
mulSingle_eq_one_iff.ne

Premises used: Pi.mulSingle_eq_one_iff, Iff.ne
-- Module: Mathlib.Algebra.Notation.Pi.Basic
Goal:
ι : Type u_1
M : ι → Type u_6
N : ι → Type u_7
inst : (i : ι) → One (M i)
inst_1 : (i : ι) → One (N i)
inst_2 : DecidableEq ι
f' : (i : ι) → M i → N i
hf' : ∀ (i : ι), f' i 1 = 1
i : ι
x : M i
j : ι
⊢ f' j (mulSingle (M := M) i x j) = mulSingle (M := N) i (f' i x) j

Tactic:
simpa only [Pi.one_apply, hf', mulSingle] using Function.apply_update f' 1 i x j

Premises used: Function.apply_update, Pi.one_apply, OfNat.ofNat, Pi.mulSingle