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

Goal state before:
pp: α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝ ∧ snd✝¹ = snd✝

Tactic:
constructor

Goal state after:
case left
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ fst✝¹ = fst✝

case right
α : Type u_4
p : α → Prop
inst✝ : DecidablePred p
fst✝¹ : Perm { a // p a }
snd✝¹ : Perm { a // ¬p a }
fst✝ : Perm { a // p a }
snd✝ : Perm { a // ¬p a }
h : (subtypeCongrHom p) (fst✝¹, snd✝¹) = (subtypeCongrHom p) (fst✝, snd✝)
⊢ snd✝¹ = snd✝
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
a b : M₀
h : a ≠ 0 → b = 0
this : Decidable (a = 0)
⊢ a * b = 0

Tactic:
exact if ha : a = 0 then by rw [ha, zero_mul] else by rw [h ha, mul_zero]

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n)

Tactic:
ext

Goal state after:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulLeft a ^ n) x✝ = (Equiv.mulLeft (a ^ n)) x✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: α : Type u_4
inst✝ : Group α
a : α
n : ℕ
⊢ Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)

Tactic:
ext

Goal state after:
α : Type u_4
inst✝ : Group α
a : α
n : ℕ
x✝ : α
⊢ (Equiv.mulRight a ^ n) x✝ = (Equiv.mulRight (a ^ n)) x✝
Module: Mathlib.Algebra.GroupWithZero.InjSurj

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
M₀' : Type u_3
G₀' : Type u_4
inst✝⁷ : GroupWithZero G₀
inst✝⁶ : Zero G₀'
inst✝⁵ : Mul G₀'
inst✝⁴ : One G₀'
inst✝³ : Inv G₀'
inst✝² : Div G₀'
inst✝¹ : Pow G₀' ℕ
inst✝ : Pow G₀' ℤ
h01 : 0 ≠ 1
f : G₀ → G₀'
hf : Surjective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : G₀), f (x * y) = f x * f y
inv : ∀ (x : G₀), f x⁻¹ = (f x)⁻¹
div : ∀ (x y : G₀), f (x / y) = f x / f y
npow : ∀ (x : G₀) (n : ℕ), f (x ^ n) = f x ^ n
zpow : ∀ (x : G₀) (n : ℤ), f (x ^ n) = f x ^ n
⊢ 0⁻¹ = 0

Tactic:
by rw [← zero, ← inv, inv_zero]

Goal state after:
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
⊢ { toFun := fun h ↦ 1 * h * 1⁻¹, invFun := fun h ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } = 1

Tactic:
ext

Goal state after:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝ : G
⊢ { toFun := fun h ↦ 1 * h * 1⁻¹, invFun := fun h ↦ 1⁻¹ * h * 1, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ } x✝ =
    1 x✝
Module: Mathlib.Algebra.Group.End

Goal state before:
pp: A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝¹ x✝ : G
⊢ { toFun := fun h ↦ x✝¹ * x✝ * h * (x✝¹ * x✝)⁻¹, invFun := fun h ↦ (x✝¹ * x✝)⁻¹ * h * (x✝¹ * x✝), left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯ } =
    { toFun := fun h ↦ x✝¹ * h * x✝¹⁻¹, invFun := fun h ↦ x✝¹⁻¹ * h * x✝¹, left_inv := ⋯, right_inv := ⋯,
        map_mul' := ⋯ } *
      { toFun := fun h ↦ x✝ * h * x✝⁻¹, invFun := fun h ↦ x✝⁻¹ * h * x✝, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Tactic:
ext

Goal state after:
A : Type u_1
M : Type u_2
G : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
inst✝¹ : Mul M
inst✝ : Group G
x✝² x✝¹ x✝ : G
⊢ { toFun := fun h ↦ x✝² * x✝¹ * h * (x✝² * x✝¹)⁻¹, invFun := fun h ↦ (x✝² * x✝¹)⁻¹ * h * (x✝² * x✝¹), left_inv := ⋯,
        right_inv := ⋯, map_mul' := ⋯ }
      x✝ =
    ({ toFun := fun h ↦ x✝² * h * x✝²⁻¹, invFun := fun h ↦ x✝²⁻¹ * h * x✝², left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ } *
        { toFun := fun h ↦ x✝¹ * h * x✝¹⁻¹, invFun := fun h ↦ x✝¹⁻¹ * h * x✝¹, left_inv := ⋯, right_inv := ⋯,
          map_mul' := ⋯ })
      x✝
Module: Mathlib.Algebra.GroupWithZero.Action.Defs

Goal state before:
pp: M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬g⁻¹ • g • 0 * g⁻¹ • (g • 0)⁻¹ = 1

Tactic:
inv_smul_smul,

Goal state after:
M : Type u_1
M₀ : Type u_2
M₀' : Type u_3
G₀ : Type u_4
G₀' : Type u_5
N : Type u_6
A : Type u_7
A' : Type u_8
B : Type u_9
α : Type u_10
β : Type u_11
inst✝² : Group α
inst✝¹ : GroupWithZero β
inst✝ : MulDistribMulAction α β
g : α
⊢ ¬0 * g⁻¹ • (g • 0)⁻¹ = 1
Module: Mathlib.Algebra.Module.Defs

Goal state before:
pp: R : Type u_5
inst✝¹ : Semiring R
M : Type u_6
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
⊢ P = Q

Tactic:
ext

Goal state after:
R : Type u_5
inst✝¹ : Semiring R
M : Type u_6
inst✝ : AddCommMonoid M
P Q : Module R M
w : ∀ (r : R) (m : M), r • m = r • m
x✝¹ : R
x✝ : M
⊢ SMul.smul x✝¹ x✝ = SMul.smul x✝¹ x✝
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (a + 1) * b = a * b + b

Tactic:
by
  rw [add_mul, one_mul]

Goal state after:
Module: Mathlib.Algebra.Ring.Defs

Goal state before:
pp: α : Type u
inst✝² : Add α
inst✝¹ : MulOneClass α
inst✝ : RightDistribClass α
a b : α
⊢ (1 + a) * b = b + a * b

Tactic:
by
  rw [add_mul, one_mul]

Goal state after:
Module: Mathlib.Data.Int.Sqrt

Goal state before:
pp: n : ℤ
⊢ ↑(↑(n.natAbs * n.natAbs)).toNat.sqrt = ↑n.natAbs

Tactic:
toNat_natCast,

Goal state after:
n : ℤ
⊢ ↑(n.natAbs * n.natAbs).sqrt = ↑n.natAbs
Module: Mathlib.Algebra.Group.Even

Goal state before:
pp: α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ ↔ IsSquare a

Tactic:
constructor

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a⁻¹ → IsSquare a

case mpr
α : Type u_2
inst✝ : DivisionMonoid α
a : α
⊢ IsSquare a → IsSquare a⁻¹
Module: Mathlib.Data.Nat.Cast.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonAssocSemiring α
m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n

Tactic:
induction n <;> simp [mul_add, *]

Goal state after:
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
⊢ g.comp 0 = 0

Tactic:
ext

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
g : β →ₙ+* γ
x✝ : α
⊢ (g.comp 0) x✝ = 0 x✝
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
⊢ comp 0 f = 0

Tactic:
ext

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : NonUnitalNonAssocSemiring β
inst✝ : NonUnitalNonAssocSemiring γ
f : α →ₙ+* β
x✝ : α
⊢ (comp 0 f) x✝ = 0 x✝
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
⊢ ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f

Tactic:
ext

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x✝ : β
⊢ ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) x✝ = f x✝
Module: Mathlib.Algebra.GroupWithZero.Commute

Goal state before:
pp: M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b c : M₀
ha : IsUnit a
k : ℕ
⊢ a⁻¹ʳ ^ k * b = c ↔ b = a ^ k * c

Tactic:
by
  rw [Ring.inverse_pow, Ring.inverse_mul_eq_iff_eq_mul _ _ _ (IsUnit.pow _ ha)]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝ : MonoidWithZero M₀
a : M₀
h : IsUnit a⁻¹ʳ
⊢ IsUnit a

Tactic:
cases subsingleton_or_nontrivial M₀
    · convert! h
    · contrapose h
      rw [Ring.inverse_non_unit _ h]
      exact not_isUnit_zero

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
h : 1 ≠ 0
⊢ mk0 1 h = 1

Tactic:
ext

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
h : 1 ≠ 0
⊢ ↑(mk0 1 h) = ↑1
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ mk0 (x * y) hxy = mk0 x ⋯ * mk0 y ⋯

Tactic:
ext

Goal state after:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
x y : G₀
hxy : x * y ≠ 0
⊢ ↑(mk0 (x * y) hxy) = ↑(mk0 x ⋯ * mk0 y ⋯)
Module: Mathlib.Algebra.GroupWithZero.Units.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
conv_lhs => rw [← mul_left_inj' hb, div_mul_cancel₀ _ hb]

Goal state after:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a b c d : G₀
hb : b ≠ 0
hc : c ≠ 0
⊢ a = c / d * b ↔ a / c = b / d
Module: Mathlib.Algebra.Ring.Commute

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
a b : R
inst✝ : NoZeroDivisors R
h : Commute a b
⊢ a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b

Tactic:
rw [← sub_eq_zero, h.sq_sub_sq, mul_eq_zero, add_eq_zero_iff_eq_neg, sub_eq_zero, or_comm]

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : S → R
hf : Injective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
x y z : S
⊢ f ((x + y) * z) = f (x * z + y * z)

Tactic:
simp only [*, right_distrib]

Goal state after:
Module: Mathlib.Algebra.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
f : S → R
hf : Injective f
inst✝⁴ : Add S
inst✝³ : Mul S
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
x y z : S
⊢ f ((x + y) * z) = f (x * z + y * z)

Tactic:
by simp only [*, right_distrib]

Goal state after:
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * k) + (-(2 * 1) + 1)

Tactic:
two_mul (1 : α),

Goal state after:
case h
α : Type u_2
inst✝ : Ring α
a k : α
hk : a = 2 * k + 1
⊢ -a = -(2 * k) + (-(1 + 1) + 1)
Module: Mathlib.Algebra.Order.Sub.Defs

Goal state before:
pp: case a
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c

Tactic:
· rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosStrictMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
lt : ∀ {x y : β}, f x < f y ↔ x < y
a : β
ha : 0 < a
b c : β
hbc : b < c
⊢ b * a < c * a

Tactic:
rw [← lt, mul, mul]; exact mul_lt_mul_of_pos_right (lt.2 hbc) (by rwa [← zero, lt])

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ a * b = c * d ↔ a = c ∧ b = d

Tactic:
rw [le_antisymm_iff, eq_true (mul_le_mul' hac hbd), true_and, mul_le_mul_iff_of_ge hac hbd]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case ha
α : Type u_1
inst✝⁵ : MulZeroClass α
a b c d : α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulReflectLE α
inst✝² : MulPosReflectLE α
inst✝¹ : PosMulMono α
inst✝ : MulPosMono α
ha : 0 < a
hc : 0 < c
hab : a ≤ b
hcd : c ≤ d
h : b * d ≤ a * c
⊢ 0 ≤ a

Tactic:
· exact ha.le

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_2
inst✝² : MonoidWithZero M₀
inst✝¹ : PartialOrder M₀
a : M₀
inst✝ : PosMulStrictMono M₀
ha : 0 < a
⊢ 0 < a ^ 2

Tactic:
by
  simpa only [sq] using mul_pos ha ha

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

Goal state before:
pp: α : Sort ?u.9
β : Type ?u.24
x✝ : α ≃ β
⊢ (fun f ↦ (↑f).equivOfSurjective ⋯) ((fun f ↦ ⟨f.toEmbedding, ⋯⟩) x✝) = x✝

Tactic:
ext

Goal state after:
α : Sort ?u.9
β : Type ?u.24
x✝¹ : α ≃ β
x✝ : α
⊢ ((fun f ↦ (↑f).equivOfSurjective ⋯) ((fun f ↦ ⟨f.toEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: one : Type u_1
α : Type u_2
inst✝ : Unique one
f : one ↪ α
⊢ (fun a ↦ { toFun := fun x ↦ a, inj' := ⋯ }) ((fun f ↦ f default) f) = f

Tactic:
ext

Goal state after:
one : Type u_1
α : Type u_2
inst✝ : Unique one
f : one ↪ α
x✝ : one
⊢ ((fun a ↦ { toFun := fun x ↦ a, inj' := ⋯ }) ((fun f ↦ f default) f)) x✝ = f x✝
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u
γ : Sort w
inst✝ : Inhabited γ
⊢ (Embedding.refl α).arrowCongrLeft = Embedding.refl (α → γ)

Tactic:
ext

Goal state after:
α : Sort u
γ : Sort w
inst✝ : Inhabited γ
x✝¹ : α → γ
x✝ : α
⊢ (Embedding.refl α).arrowCongrLeft x✝¹ x✝ = (Embedding.refl (α → γ)) x✝¹ x✝
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
⊢ (fun f ↦ Embedding.congr h.symm h'.symm f) ((fun f ↦ Embedding.congr h h' f) x) = x

Tactic:
ext

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : α ↪ γ
x✝ : α
⊢ ((fun f ↦ Embedding.congr h.symm h'.symm f) ((fun f ↦ Embedding.congr h h' f) x)) x✝ = x x✝
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
⊢ (fun f ↦ Embedding.congr h h' f) ((fun f ↦ Embedding.congr h.symm h'.symm f) x) = x

Tactic:
ext

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
δ : Sort u_4
h : α ≃ β
h' : γ ≃ δ
x : β ↪ δ
x✝ : β
⊢ ((fun f ↦ Embedding.congr h h' f) ((fun f ↦ Embedding.congr h.symm h'.symm f) x)) x✝ = x x✝
Module: Mathlib.Logic.Embedding.Basic

Goal state before:
pp: α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
⊢ (ea.embeddingCongr ec) (f.trans g) = ((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)

Tactic:
ext

Goal state after:
α₁ : Sort u_1
β₁ : Sort u_2
γ₁ : Sort u_3
α₂ : Sort u_4
β₂ : Sort u_5
γ₂ : Sort u_6
ea : α₁ ≃ α₂
eb : β₁ ≃ β₂
ec : γ₁ ≃ γ₂
f : α₁ ↪ β₁
g : β₁ ↪ γ₁
x✝ : α₂
⊢ ((ea.embeddingCongr ec) (f.trans g)) x✝ = (((ea.embeddingCongr eb) f).trans ((eb.embeddingCongr ec) g)) x✝
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ 0 < a * a ↔ a ≠ 0

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ 0 < a * a → a ≠ 0

case mpr
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ a ≠ 0 → 0 < a * a
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : ExistsAddOfLE R
inst✝¹ : PosMulMono R
inst✝ : AddLeftMono R
a : R
⊢ 0 ≤ a ^ 2

Tactic:
by
  obtain ha | ha := le_or_gt 0 a
  · exact pow_succ_nonneg ha _
  obtain ⟨b, hab⟩ := exists_add_of_le ha.le
  have hb : 0 < b := not_le.1 fun hb ↦ (add_neg_of_neg_of_nonpos ha hb).ne' hab
  calc
    0 ≤ b ^ 2 := pow_succ_nonneg hb.le _
    _ = b ^ 2 + a * (a + b) := by rw [← hab, mul_zero, add_zero]
    _ = a ^ 2 + (a + b) * b := by rw [add_mul, mul_add, sq, sq, add_comm, add_assoc]
    _ = a ^ 2 := by rw [← hab, zero_mul, add_zero]

Goal state after:
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b : G₀
ha : 0 < a
hb : 0 < b
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rw [inv_lt_iff_one_lt_mul₀' ha, lt_mul_inv_iff₀ hb, one_mul]

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
x y : Quotient x✝
⊢ r ((Embedding.quotientOut α) x) ((Embedding.quotientOut α) y) ↔ Quotient.lift₂ r H x y

Tactic:
induction x, y using Quotient.inductionOn₂
    apply iff_iff_eq.2 (H _ _ _ _ _ _) <;> apply Quotient.mk_out

Goal state after:
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ ↔ Acc r a

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc (Quotient.lift₂ r H) ⟦a⟧ → Acc r a

case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
a : α
⊢ Acc r a → Acc (Quotient.lift₂ r H) ⟦a⟧
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) ↔ WellFounded r

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded (Quotient.lift₂ r H) → WellFounded r

case mpr
α : Type u_1
x✝ : Setoid α
r : α → α → Prop
H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ ≈ a₂ → b₁ ≈ b₂ → r a₁ b₁ = r a₂ b₂
⊢ WellFounded r → WellFounded (Quotient.lift₂ r H)
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝ : r ≃r s
⊢ (fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝) = x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
x✝¹ : r ≃r s
x✝ : α
⊢ ((fun f ↦ ofSurjective ↑f ⋯) ((fun f ↦ ⟨f.toRelEmbedding, ⋯⟩) x✝¹)) x✝ = x✝¹ x✝
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
⊢ (fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom))
      ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)) f₁) =
    f₁

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ →r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom))
        ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)) f₁))
      x✝ =
    f₁ x✝
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ →r s₂
⊢ (fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom))
      ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom)) f₂) =
    f₂

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ →r s₂
x✝ : α₂
⊢ ((fun f₁ ↦ e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom))
        ((fun f₂ ↦ e₂.symm.toRelEmbedding.toRelHom.comp (f₂.comp e₁.toRelEmbedding.toRelHom)) f₂))
      x✝ =
    f₂ x✝
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ↪r s₁
⊢ (fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding)
      ((fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding) f₁) =
    f₁

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ↪r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding)
        ((fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding) f₁))
      x✝ =
    f₁ x✝
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ↪r s₂
⊢ (fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding)
      ((fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding) f₂) =
    f₂

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₂ : r₂ ↪r s₂
x✝ : α₂
⊢ ((fun f₁ ↦ (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding)
        ((fun f₂ ↦ (e₁.toRelEmbedding.trans f₂).trans e₂.symm.toRelEmbedding) f₂))
      x✝ =
    f₂ x✝
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ≃r s₁
⊢ (fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) ((fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) f₁) = f₁

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.51
β₁ : Type ?u.54
α₂ : Type ?u.50
β₂ : Type ?u.53
r₁ : α₁ → α₁ → Prop
s₁ : β₁ → β₁ → Prop
r₂ : α₂ → α₂ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r r₂
e₂ : s₁ ≃r s₂
f₁ : r₁ ≃r s₁
x✝ : α₁
⊢ ((fun f₂ ↦ (e₁.trans f₂).trans e₂.symm) ((fun f₁ ↦ (e₁.symm.trans f₁).trans e₂) f₁)) x✝ = f₁ x✝