awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
x : κ
hfg : ¬x ∈ f '' mulSupport g
hf : ¬∃ (a : ι), f a = x
⊢ Eq.{u_4 + 1} (α := N) (1 x) 1

Tactic:
rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
N : Type u_4
inst : One N
f : ι → κ
g : ι → N
hf : Injective f
x : ι
hx : x ∈ mulSupport g
rwa : extend f g 1 (f x) ≠ 1
rwa₁ rwa₂ rwa₃ rwa₄ : g x ≠ 1
⊢ f x ∈ mulSupport (extend f g 1)

Tactic:
rwa [mem_mulSupport, hf.extend_apply]

Premises used: Function.mem_mulSupport, Function.Injective.extend_apply
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
simp_rw : mulSupport f ⊆ sᶜ ↔ EqOn f 1 s
simp_rw₁ : (∀ (x : ι), ¬x ∈ sᶜ → f x = 1) ↔ EqOn f 1 s
simp_rw₂ : (∀ (x : ι), x ∈ s → f x = 1) ↔ EqOn f 1 s
simp_rw₃ : (∀ (x : ι), x ∈ s → f x = 1) ↔ ∀ ⦃x : ι⦄, x ∈ s → f x = 1 x
⊢ Disjoint (mulSupport f) s ↔ EqOn f 1 s

Tactic:
simp_rw [← subset_compl_iff_disjoint_right, mulSupport_subset_iff', notMem_compl_iff, EqOn,
    Pi.one_apply]

Premises used: Set.subset_compl_iff_disjoint_right, Pi.one_apply, Function.mulSupport_subset_iff', Set.EqOn, Set.notMem_compl_iff
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
s : Set ι
rw : Disjoint (mulSupport f) s ↔ EqOn f 1 s
rw₁ rw₂ : EqOn f 1 s ↔ EqOn f 1 s
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s

Tactic:
rw [disjoint_comm, mulSupport_disjoint_iff]

Premises used: disjoint_comm, Function.mulSupport_disjoint_iff
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
rw : (∀ (x : ι), ¬Membership.mem (γ := Set ι) ∅ x → f x = 1) ↔ ∀ (x : ι), f x = 1 x
⊢ mulSupport f = ∅ ↔ f = 1

Tactic:
rw [← subset_empty_iff, mulSupport_subset_iff', funext_iff]

Premises used: funext_iff, Function.mulSupport_subset_iff', Set.subset_empty_iff
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
⊢ (∀ (x : ι), ¬Membership.mem (γ := Set ι) ∅ x → f x = 1) ↔ ∀ (x : ι), f x = 1 x

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
rw : mulSupport f ≠ ∅ ↔ f ≠ 1
rw₁ : ¬mulSupport f = ∅ ↔ f ≠ 1
rw₂ rw₃ : ¬f = 1 ↔ f ≠ 1
⊢ (mulSupport f).Nonempty ↔ f ≠ 1

Tactic:
rw [nonempty_iff_ne_empty, Ne, mulSupport_eq_empty_iff]

Premises used: Ne, Set.nonempty_iff_ne_empty, Function.mulSupport_eq_empty_iff
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
inst_1 : Subsingleton M
f : ι → M
⊢ mulSupport f = ∅

Tactic:
mulSupport_eq_empty_iff.mpr <| Subsingleton.elim f 1

Premises used: Iff.mpr, Function.mulSupport_eq_empty_iff, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
⊢ range f ⊆ insert 1 (f '' mulSupport f)

Tactic:
simpa only [range_subset_iff, mem_insert_iff, or_iff_not_imp_left] using
    fun x (hx : x ∈ mulSupport f) ↦ mem_image_of_mem f hx

Premises used: Set.mem_image_of_mem, Classical.or_iff_not_imp_left, Set.mem_insert_iff, Set.range_subset_iff
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
⊢ range f ⊆ insert 1 (f '' k)

Tactic:
have : range f ⊆ insert 1 (f '' k) :=
    (range_subset_insert_image_mulSupport f).trans (insert_subset_insert (image_mono h))
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
k : Set ι
h : mulSupport f ⊆ k
this : range f ⊆ insert 1 (f '' k)
⊢ range f = f '' k ∨ range f = insert 1 (f '' k)

Tactic:
grind
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
⊢ Eq.{u_1 + 1} (α := Set ι) (mulSupport.{u_1, u_3} (M := M) 1) ∅

Tactic:
mulSupport_eq_empty_iff.2 rfl

Premises used: Iff.mpr, Function.mulSupport_eq_empty_iff, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
⊢ Eq.{u_1 + 1} (α := Set ι) (mulSupport.{u_1, u_3} (M := M) fun (x : ι) ↦ 1) ∅

Tactic:
mulSupport_one

Premises used: Function.mulSupport_one
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
c : M
hc : c ≠ 1
h :
  ∀ (x : ι),
    Membership.mem (γ := Set ι) (mulSupport.{u_1, u_3} (M := M) fun (x : ι) ↦ c) x ↔ Membership.mem (γ := Set ι) univ x
⊢ Eq.{u_1 + 1} (α := Set ι) (mulSupport.{u_1, u_3} (M := M) fun (x : ι) ↦ c) univ

Tactic:
ext x
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
c : M
hc : c ≠ 1
x : ι
⊢ Membership.mem (γ := Set ι) (mulSupport.{u_1, u_3} (M := M) fun (x : ι) ↦ c) x ↔ Membership.mem (γ := Set ι) univ x

Tactic:
simp [hc]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : One M
f : ι → M
hf : ∀ (x : ι), f x ≠ 1
⊢ mulSupport f = univ

Tactic:
Set.eq_univ_of_forall hf

Premises used: Set.eq_univ_of_forall
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
P : Type u_5
inst : One M
inst_1 : One N
inst_2 : One P
op : M → N → P
op1 : op 1 1 = 1
f : ι → M
g : ι → N
x : ι
hx : Membership.mem (γ := Set ι) (mulSupport.{u_1, u_5} (M := P) fun (x : ι) ↦ op (f x) (g x)) x
hf : f x = 1
hg : g x = 1
⊢ Eq.{u_5 + 1} (α := P) ((fun (x : ι) ↦ op (f x) (g x)) x) 1

Tactic:
simp only [hf, hg, op1]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
g : M → N
hg : g 1 = 1
f : ι → M
x : ι
h : f x = 1
⊢ (g ∘ f) x = 1

Tactic:
simp only [(· ∘ ·), *]

Premises used: Function.comp
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
g : M → N
hg : ∀ {x : M}, g x = 1 → x = 1
f : ι → M
⊢ mulSupport f ⊆ mulSupport (g ∘ f)

Tactic:
fun _ ↦ mt hg

Premises used: Set.Mem, setOf, mt, Set.Subset, Function.mulSupport, Not
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
g : M → N
hg : ∀ {x : M}, g x = 1 ↔ x = 1
f : ι → M
⊢ mulSupport (g ∘ f) = mulSupport f

Tactic:
Set.ext fun _ ↦ not_congr hg

Premises used: Set.ext, not_congr
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
g : M → N
f : ι → M
hg : ∀ {x : M}, x ∈ range f → (g x = 1 ↔ x = 1)
x : ι
rw : g (f x) = 1 ↔ f x = 1
rw₁ rw₂ : f x = 1 ↔ f x = 1
⊢ (g ∘ f) x = 1 ↔ f x = 1

Tactic:
rw [Function.comp, hg (mem_range_self x)]

Premises used: Set.mem_range_self, Function.comp
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : One M
g : κ → M
f : ι → κ
⊢ mulSupport (g ∘ f) = f ⁻¹' mulSupport g

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Function.mulSupport, Not, rfl
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
f : ι → M
g : ι → N
x : ι
⊢ Membership.mem (γ := Set ι) (mulSupport (M := M × N) fun (x : ι) ↦ (f x, g x)) x ↔ x ∈ mulSupport f ∪ mulSupport g

Tactic:
simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne]

Premises used: Set.mem_union, Prod.mk_eq_one, Ne, Set.mem_setOf_eq, not_and_or, Function.mulSupport
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
N : Type u_4
inst : One M
inst_1 : One N
f : ι → M × N
⊢ mulSupport f =
    (mulSupport.{u_1, u_3} (M := M) fun (x : ι) ↦ (f x).1) ∪ mulSupport.{u_1, u_4} (M := N) fun (x : ι) ↦ (f x).2

Tactic:
simp only [← mulSupport_prodMk]

Premises used: Function.mulSupport_prodMk
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : One M
f : ι × κ → M
i : ι
j : κ
hj : Membership.mem (γ := Set κ) (mulSupport.{u_2, u_3} (M := M) fun (j : κ) ↦ f (i, j)) j
⊢ (i, j) ∈ mulSupport f ∧ (i, j).2 = j

Tactic:
simpa using hj
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : One M
f : ι × κ → M
⊢ mulSupport (curry f) = Prod.fst '' mulSupport f

Tactic:
simp [mulSupport, funext_iff, image]

Premises used: funext_iff, Function.mulSupport, Set.image
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : One M
f : ι × κ → M
⊢ (mulSupport (M := (j : κ) → M) fun (i : ι) (j : κ) ↦ f (i, j)) = Prod.fst '' mulSupport f

Tactic:
mulSupport_curry f

Premises used: Function.mulSupport_curry
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst : One M
f : ι → M
s : Set κ
g : κ → ι
rw : g '' s ∩ mulSupport f = g '' (s ∩ g ⁻¹' mulSupport f)
rw₁ rw₂ : g '' s ∩ mulSupport f = g '' s ∩ mulSupport f
⊢ g '' s ∩ mulSupport f = g '' (s ∩ mulSupport (f ∘ g))

Tactic:
rw [mulSupport_comp_eq_preimage f g, image_inter_preimage]

Premises used: Set.image_inter_preimage, Function.mulSupport_comp_eq_preimage
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
⊢ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) ⊆ {i}

Tactic:
fun _ hx ↦
  by_contra fun hx' ↦ hx <| mulSingle_eq_of_ne hx' _

Premises used: Set.Subset, by_contra, Pi.mulSingle_eq_of_ne
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
⊢ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i 1) = ∅

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
h : a ≠ 1
x : ι
hx : Membership.mem (γ := Set ι) {i} x
rwa : Ne.{u_3 + 1} (α := M) (mulSingle (M := fun (a : ι) ↦ M) i a x : M) (1 : M)
rwa₁ : Ne.{u_3 + 1} (α := M) (mulSingle (M := fun (a : ι) ↦ M) i a i : M) (1 : M)
rwa₂ rwa₃ rwa₄ rwa₅ : a ≠ 1
⊢ x ∈ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a)

Tactic:
rwa [mem_mulSupport, hx, mulSingle_eq_same]

Premises used: Pi.mulSingle_eq_same, Function.mem_mulSupport
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
inst_2 : DecidableEq M
pos : ∀ (h : a = 1), mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = ∅
neg : ∀ (h : ¬a = 1), mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = {i}
⊢ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = if a = 1 then ∅ else {i}

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
inst_2 : DecidableEq M
h : a = 1
⊢ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = ∅

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
inst_2 : DecidableEq M
h : ¬a = 1
⊢ mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a) = {i}

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
rw : Set.Subsingleton (α := ι) (if a = 1 then ∅ else {i})
⊢ (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a)).Subsingleton

Tactic:
rw [mulSupport_mulSingle]

Premises used: Pi.mulSupport_mulSingle
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
pos : ∀ (h : a = 1), Set.Subsingleton.{u_1} (α := ι) ∅
neg : ∀ (h : ¬a = 1), Set.Subsingleton (α := ι) {i}
⊢ Set.Subsingleton (α := ι) (if a = 1 then ∅ else {i})

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
h : a = 1
⊢ Set.Subsingleton.{u_1} (α := ι) ∅

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
h : ¬a = 1
⊢ Set.Subsingleton (α := ι) {i}

Tactic:
simp
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i : ι
a : M
rw rw₁ rw₂ : Set.Subsingleton (α := ι) (if a = 1 then ∅ else {i})
⊢ (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a)).Subsingleton

Tactic:
classical
  rw [mulSupport_mulSingle]
  split_ifs with h <;> simp

Premises used: Pi.mulSupport_mulSingle
-- Module: Mathlib.Algebra.Notation.Support
Goal:
ι : Type u_1
M : Type u_3
inst : DecidableEq ι
inst_1 : One M
i j : ι
a b : M
ha : a ≠ 1
hb : b ≠ 1
rw : Disjoint {i} (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔ i ≠ j
rw₁ : Disjoint (α := Set ι) {i} {j} ↔ i ≠ j
rw₂ rw₃ : i ≠ j ↔ i ≠ j
⊢ Disjoint (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) i a))
      (mulSupport.{u_1, u_3} (M := M) (mulSingle (M := fun (a : ι) ↦ M) j b)) ↔
    i ≠ j

Tactic:
rw [mulSupport_mulSingle_of_ne ha, mulSupport_mulSingle_of_ne hb, disjoint_singleton]

Premises used: Set.disjoint_singleton, Pi.mulSupport_mulSingle_of_ne
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
x : α
⊢ unop (op x) = x

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
x : αᵐᵒᵖ
⊢ op (unop x) = x

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := αᵐᵒᵖ → αᵐᵒᵖ) (op ∘ unop) id

Tactic:
rfl

Premises used: MulOpposite, MulOpposite.unop, rfl, MulOpposite.op
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α → α) (unop ∘ op) id

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := α) op

Tactic:
opEquiv.bijective

Premises used: MulOpposite.opEquiv, Equiv.bijective, MulOpposite.op
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := αᵐᵒᵖ) unop

Tactic:
opEquiv.symm.bijective

Premises used: MulOpposite.opEquiv, Equiv.bijective, MulOpposite, MulOpposite.unop, Equiv.symm
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) op

Tactic:
op_bijective.injective

Premises used: Function.Bijective.injective, MulOpposite.op_bijective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := α) op

Tactic:
op_bijective.surjective

Premises used: Function.Bijective.surjective, MulOpposite.op_bijective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := αᵐᵒᵖ) unop

Tactic:
unop_bijective.injective

Premises used: Function.Bijective.injective, MulOpposite.unop_bijective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := αᵐᵒᵖ) unop

Tactic:
unop_bijective.surjective

Premises used: Function.Bijective.surjective, MulOpposite.unop_bijective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
x y : α
⊢ op x = op y ↔ x = y

Tactic:
iff_of_eq <| PreOpposite.op'.injEq _ _

Premises used: PreOpposite.op'.injEq, iff_of_eq
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
x y : αᵐᵒᵖ
⊢ unop x = unop y ↔ x = y

Tactic:
unop_injective.eq_iff

Premises used: Function.Injective.eq_iff, MulOpposite.unop_injective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
p : αᵐᵒᵖ → Prop
⊢ (∀ (a : αᵐᵒᵖ), p a) ↔ ∀ (a : α), p (op a)

Tactic:
op_surjective.forall

Premises used: Function.Surjective.forall, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
p : αᵐᵒᵖ → Prop
⊢ (∃ (a : αᵐᵒᵖ), p a) ↔ ∃ (a : α), p (op a)

Tactic:
op_surjective.exists

Premises used: Function.Surjective.exists, MulOpposite.op_surjective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
β : Type u_2
inst : Nontrivial α
⊢ Nontrivial.{u_1} αᵐᵒᵖ

Tactic:
op_injective.nontrivial

Premises used: MulOpposite.op_injective, Function.Injective.nontrivial
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
β : Type u_2
inst : Subsingleton α
⊢ Subsingleton.{u_1 + 1} αᵐᵒᵖ

Tactic:
unop_injective.subsingleton

Premises used: Function.Injective.subsingleton, MulOpposite.unop_injective
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
β : Type u_2
inst : IsEmpty α
⊢ IsEmpty.{u_1 + 1} αᵐᵒᵖ

Tactic:
Function.isEmpty unop

Premises used: Function.isEmpty, MulOpposite.unop
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Add α
simp_rw : IsLeftCancelAdd.{u_1} αᵐᵒᵖ ∧ IsRightCancelAdd.{u_1} αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α
simp_rw₁ : IsLeftCancelAdd α ∧ IsRightCancelAdd.{u_1} αᵐᵒᵖ ↔ IsLeftCancelAdd α ∧ IsRightCancelAdd α
⊢ IsCancelAdd.{u_1} αᵐᵒᵖ ↔ IsCancelAdd α

Tactic:
simp_rw [isCancelAdd_iff, isLeftCancelAdd_iff, isRightCancelAdd_iff]

Premises used: isCancelAdd_iff, MulOpposite.isLeftCancelAdd_iff, MulOpposite.isRightCancelAdd_iff
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Zero α
⊢ Eq.{u_1 + 1} (α := αᵐᵒᵖ) (op 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Zero α
⊢ Eq.{u_1 + 1} (α := α) (unop 0) 0

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := αᵐᵒᵖ) (op 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Add α
x y : α
⊢ op (x + y) = op x + op y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Add α
x y : αᵐᵒᵖ
⊢ unop (x + y) = unop x + unop y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Neg α
x : α
⊢ op (-x) = -op x

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Neg α
x : αᵐᵒᵖ
⊢ unop (-x) = -unop x

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Mul α
x y : α
⊢ op (x * y) = op y * op x

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Mul α
x y : αᵐᵒᵖ
⊢ unop (x * y) = unop y * unop x

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Inv α
x : α
⊢ op x⁻¹ = (op x)⁻¹

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Inv α
x : αᵐᵒᵖ
⊢ unop x⁻¹ = (unop x)⁻¹

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Sub α
x y : α
⊢ op (x - y) = op x - op y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Sub α
x y : αᵐᵒᵖ
⊢ unop (x - y) = unop x - unop y

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
a : α
b : β
⊢ op (a • b) = a • op b

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
β : Type u_2
inst : SMul α β
a : α
b : βᵐᵒᵖ
⊢ unop (a • b) = a • unop b

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Zero α
a : αᵐᵒᵖ
⊢ unop a = 0 ↔ a = 0

Tactic:
unop_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', MulOpposite.unop_injective, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Zero α
a : α
⊢ op a = 0 ↔ a = 0

Tactic:
op_injective.eq_iff' rfl

Premises used: MulOpposite.op_injective, Function.Injective.eq_iff', rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Zero α
a : αᵐᵒᵖ
⊢ unop a ≠ 0 ↔ a ≠ 0

Tactic:
not_congr <| unop_eq_zero_iff a

Premises used: not_congr, MulOpposite.unop_eq_zero_iff
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Zero α
a : α
⊢ op a ≠ 0 ↔ a ≠ 0

Tactic:
not_congr <| op_eq_zero_iff a

Premises used: MulOpposite.op_eq_zero_iff, not_congr
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
a : αᵐᵒᵖ
⊢ unop a = 1 ↔ a = 1

Tactic:
unop_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', MulOpposite.unop_injective, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
a : α
⊢ op a = 1 ↔ a = 1

Tactic:
op_injective.eq_iff

Premises used: MulOpposite.op_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := αᵃᵒᵖ) (op 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := α) (unop 1) 1

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
a : α
⊢ op a = 1 ↔ a = 1

Tactic:
op_injective.eq_iff

Premises used: AddOpposite.op_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : One α
a : αᵃᵒᵖ
⊢ unop a = 1 ↔ a = 1

Tactic:
unop_injective.eq_iff

Premises used: Function.Injective.eq_iff, AddOpposite.unop, AddOpposite.unop_injective, AddOpposite.op
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Mul α
a b : α
⊢ op (a * b) = op a * op b

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Mul α
a b : αᵃᵒᵖ
⊢ unop (a * b) = unop a * unop b

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Inv α
a : α
⊢ op a⁻¹ = (op a)⁻¹

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Inv α
a : αᵃᵒᵖ
⊢ unop a⁻¹ = (unop a)⁻¹

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Div α
a b : α
⊢ op (a / b) = op a / op b

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Opposites
Goal:
α : Type u_1
inst : Div α
a b : αᵃᵒᵖ
⊢ unop (a / b) = unop a / unop b

Tactic:
rfl

Premises used: AddOpposite.unop, rfl
-- Module: Mathlib.Algebra.Order.AbsoluteValue.Basic
Goal:
ι : Type u_1
α : Type u_2
R_1 : Type u_3
S_1 : Type u_4
R : Type u_5
S : Type u_6
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
abv f g : AbsoluteValue R S
h : Eq (α := (a : R) → S) ((fun (f : AbsoluteValue R S) ↦ f.toFun) f) ((fun (f : AbsoluteValue R S) ↦ f.toFun) g)
obtain :
  ∀ (toFun : R → S) (map_mul' : ∀ (x y : R), toFun (x * y) = toFun x * toFun y)
    (nonneg' : ∀ (x : R), 0 ≤ { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x)
    (eq_zero' : ∀ (x : R), { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x = 0 ↔ x = 0)
    (add_le' :
      ∀ (x y : R),
        { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun (x + y) ≤
          { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun x +
            { toFun := toFun, map_mul' := map_mul' : R →ₙ* S }.toFun y)
    (h :
      Eq (α := (a : R) → S)
        ((fun (f : AbsoluteValue R S) ↦ f.toFun)
          { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' })
        ((fun (f : AbsoluteValue R S) ↦ f.toFun) g)),
    { toFun := toFun, map_mul' := map_mul', nonneg' := nonneg', eq_zero' := eq_zero', add_le' := add_le' :
        AbsoluteValue R S } =
      g
⊢ f = g

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := f