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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ e.symm x = y ↔ x = e y

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
e : α ≃ β
x : β
y : α
⊢ y = e.symm x ↔ e y = x

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans (Equiv.refl β) = e

Tactic:
grind

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

Goal state before:
pp: case mk
α : Sort u
β : Sort v
toFun✝ : α → β
invFun✝ : β → α
left_inv✝ : LeftInverse invFun✝ toFun✝
right_inv✝ : RightInverse invFun✝ toFun✝
⊢ (Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =
    { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
rfl

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

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.symm.trans e = Equiv.refl β

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
e : α ≃ β
⊢ e.trans e.symm = Equiv.refl α

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
bc : β ≃ γ
cd : γ ≃ δ
⊢ (ab.trans bc).trans cd = ab.trans (bc.trans cd)

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ f = e.symm.trans g

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
e : α ≃ β
f : β ≃ γ
g : α ≃ γ
⊢ e.trans f = g ↔ e = g.trans f.symm

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
ac : α ≃ γ
⊢ (fun bd ↦ ab.trans (bd.trans cd.symm)) ((fun ac ↦ (ab.symm.trans ac).trans cd) ac) = ac

Tactic:
grind

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

Goal state before:
pp: case zero
α : Type u
f g : α → α
h : Commute f g
⊢ (f ∘ g)^[0] = f^[0] ∘ g^[0]

Tactic:
rfl

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
ac : β ≃ δ
⊢ (fun ac ↦ (ab.symm.trans ac).trans cd) ((fun bd ↦ ab.trans (bd.trans cd.symm)) ac) = ac

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ab : α ≃ β
cd : γ ≃ δ
x✝¹ : β ≃ δ
x✝ : α
⊢ ((ab.equivCongr cd).symm x✝¹) x✝ = ((ab.symm.equivCongr cd.symm) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
⊢ (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
δ : Sort u_1
ε : Sort u_2
ζ : Sort u_3
ab : α ≃ β
de : δ ≃ ε
bc : β ≃ γ
ef : ε ≃ ζ
⊢ (ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)

Tactic:
grind

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

Goal state before:
pp: α' : Type u_1
β' : Type u_2
e : α' ≃ β'
p p' : Perm α'
⊢ Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')

Tactic:
grind

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

Goal state before:
pp: α : Type u
f : α → α
n : ℕ
x : α
⊢ (f ∘ f^[n]) x = f (f^[n] x)

Tactic:
rfl

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₁ → β₁
⊢ (fun f ↦ ⇑e₂.symm ∘ f ∘ ⇑e₁) ((fun f ↦ ⇑e₂ ∘ f ∘ ⇑e₁.symm) f) = f

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
α₁ : Sort u_1
β₁ : Sort u_2
α₂ : Sort u_3
β₂ : Sort u_4
e₁ : α₁ ≃ α₂
e₂ : β₁ ≃ β₂
f : α₂ → β₂
⊢ (fun f ↦ ⇑e₂ ∘ f ∘ ⇑e₁.symm) ((fun f ↦ ⇑e₂.symm ∘ f ∘ ⇑e₁) f) = f

Tactic:
grind

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

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.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f

Tactic:
grind

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

Goal state before:
pp: case refl
α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ uniqueElim ((fun f ↦ f default) f) default = f default

Tactic:
rfl

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ LeftInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : Sort v
γ : Sort w
β₁ : α → Sort u_1
β₂ : α → Sort u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ RightInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
grind

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

Goal state before:
pp: α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ LeftInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
grind

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

Goal state before:
pp: α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.20
β₁ : α → Type u_1
β₂ : α → Type u_2
F : (a : α) → β₁ a ≃ β₂ a
⊢ RightInverse (fun a ↦ ⟨a.fst, (F a.fst).symm a.snd⟩) fun a ↦ ⟨a.fst, (F a.fst) a.snd⟩

Tactic:
grind

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

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

Tactic:
rfl

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

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

Tactic:
rfl

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:
grind

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:
grind

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

Goal state before:
pp: case neg
ι : 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 : ι
h : ¬j = i
⊢ f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j

Tactic:
simp only [mulSingle_eq_of_ne h, hf']

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:
grind

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

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

Tactic:
rfl

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:
grind

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:
grind

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:
grind

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:
grind

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:
grind

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isLeft = true ↔ (inl c✝).isLeft = true

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isLeft = true ↔ (inr d✝).isLeft = true

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a✝¹ : α
c✝ : γ
a✝ : r a✝¹ c✝
⊢ (inl a✝¹).isRight = true ↔ (inl c✝).isRight = true

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b✝ : β
d✝ : δ
a✝ : s b✝ d✝
⊢ (inr b✝).isRight = true ↔ (inr d✝).isRight = true

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
c : γ
a✝¹ : α
a✝ : r a✝¹ c
⊢ (inl a✝¹).isLeft = true

Tactic:
rfl

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
a : α
c✝ : γ
a✝ : r a c✝
⊢ (inl c✝).isLeft = true

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
d : δ
b✝ : β
a✝ : s b✝ d
⊢ (inr b✝).isRight = true

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
r : α → γ → Prop
s : β → δ → Prop
b : β
d✝ : δ
a✝ : s b d✝
⊢ (inr d✝).isRight = true

Tactic:
rfl

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:
grind

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:
grind

Goal state after:
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Option.elim' (f none) (f ∘ some) none = f none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ Option.elim' (f none) (f ∘ some) (some val✝) = f (some val✝)

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: case none
α : Type u_3
β : Type u_4
b : β
f : α → β
⊢ Option.elim' b f none = none.elim b f

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.Defs

Goal state before:
pp: case some
α : Type u_3
β : Type u_4
b : β
f : α → β
val✝ : α
⊢ Option.elim' b f (some val✝) = (some val✝).elim b f

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
a : α
h : ∀ (a_1 : α), a_1 ∈ some a → p a_1
ha : a ∈ some a
⊢ pmap f (some a) h = some (f a ⋯)

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
inst✝ : Inhabited α
⊢ none.getD default = none.iget

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
inst✝ : Inhabited α
val✝ : α
⊢ (some val✝).getD default = (some val✝).iget

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ none.casesOn' (f none) (f ∘ fun a ↦ some a) = f none

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ (some val✝).casesOn' (f none) (f ∘ fun a ↦ some a) = f (some val✝)

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ none.casesOn' b f = none.elim b f

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
b : β
f : α → β
val✝ : α
⊢ (some val✝).casesOn' b f = (some val✝).elim b f

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
f : Option α → β
⊢ none.elim (f none) (f ∘ some) = f none

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
f : Option α → β
val✝ : α
⊢ (some val✝).elim (f none) (f ∘ some) = f (some val✝)

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
⊢ (none.elim (h x) fun j ↦ h (f j)) = h (none.elim x f)

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
f : γ → α
x : α
val✝ : γ
⊢ ((some val✝).elim (h x) fun j ↦ h (f j)) = h ((some val✝).elim x f)

Tactic:
rfl

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

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
⊢ (none.elim (h x y) fun j ↦ h (f j) (g j)) = h (none.elim x f) (none.elim y g)

Tactic:
rfl

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

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β → γ
f : γ → α
x : α
g : γ → β
y : β
val✝ : γ
⊢ ((some val✝).elim (h x y) fun j ↦ h (f j) (g j)) = h ((some val✝).elim x f) ((some val✝).elim y g)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Inv γ
f : α → β
g : α → γ
e : β → γ
x : β
⊢ extend f g⁻¹ e⁻¹ x = (extend f g e)⁻¹ x

Tactic:
simp [Function.extend_def, apply_dite Inv.inv]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : α
⊢ Sum.elim (a * a') (b * b') (inl val✝) = (Sum.elim a b * Sum.elim a' b') (inl val✝)

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Mul γ
val✝ : β
⊢ Sum.elim (a * a') (b * b') (inr val✝) = (Sum.elim a b * Sum.elim a' b') (inr val✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x : α × β
y : β × α
⊢ x.swap = y ↔ x = y.swap

Tactic:
grind

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : α
⊢ Sum.elim (a / a') (b / b') (inl val✝) = (Sum.elim a b / Sum.elim a' b') (inl val✝)

Tactic:
rfl

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
a a' : α → γ
b b' : β → γ
inst✝ : Div γ
val✝ : β
⊢ Sum.elim (a / a') (b / b') (inr val✝) = (Sum.elim a b / Sum.elim a' b') (inr val✝)

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ Prod.Lex r s (i, b) (i, a)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r✝ : α → α → Prop
s✝ : β → β → Prop
x y : α × β
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Total s
x✝¹ x✝ : α × β
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

Tactic:
obtain hij | rfl | hji := trichotomous_of r i j

Goal state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
hij : r i j
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)

case inr.inl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a b : β
⊢ Prod.Lex r s (i, a) (i, b) ∨ (i, a) = (i, b) ∨ Prod.Lex r s (i, b) (i, a)

case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
x y : α × β
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Trichotomous s
i : α
a : β
j : α
b : β
hji : r j i
⊢ Prod.Lex r s (i, a) (j, b) ∨ (i, a) = (j, b) ∨ Prod.Lex r s (j, b) (i, a)
Module: Mathlib.Order.Defs.PartialOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ (b ≤ a ∧ ∀ ⦃c : α⦄, b < c → ¬c < a) = (b ≤ a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c)

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Defs.PartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : LT α
a b : α
⊢ (b < a ∧ ∀ ⦃c : α⦄, b < c → ¬c < a) = (b < a ∧ ∀ ⦃c : α⦄, c < a → ¬b < c)

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : Nonempty α
inst✝ : Nonempty β
f : α → γ
g : β → δ
⊢ Bijective (map f g) ↔ Bijective f ∧ Bijective g

Tactic:
by
  have := Nonempty.map f ‹_›
  have := Nonempty.map g ‹_›
  exact (map_injective.and map_surjective).trans and_and_and_comm

Goal state after:
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ a

Tactic:
by
  rw [min_def]
  split_ifs with h <;> simp [h, le_of_not_ge]

Goal state after:
Module: Mathlib.Order.OrderDual

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
inst✝ : LinearOrder α
a b : αᵒᵈ
⊢ (if b < a then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
x y x' y' : α
ltc : x < y ↔ x' < y'
gtc : y < x ↔ y' < x'
⊢ x = y ↔ x' = y'

Tactic:
grind

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝¹ : f a < f b
h✝ : a < b
⊢ Ordering.lt = Ordering.lt

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False

Tactic:
rfl

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
rfl

Goal state after:
case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : f a < f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False

Tactic:
rfl

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : f a = f b
h✝ : a < b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : a = b
⊢ Ordering.eq = Ordering.eq

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False

Tactic:
rfl

Goal state after:
case neg
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝³ : ¬f a < f b
h✝² : f a = f b
h✝¹ : ¬a < b
h✝ : ¬a = b
⊢ False
Module: Mathlib.Order.Basic

Goal state before:
pp: case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False

Tactic:
rfl

Goal state after:
case pos
α : Type u_2
β : Type u_3
a b : α
inst✝² : LinearOrder β
inst✝¹ : DecidableEq α
f : α → β
inj : Injective f
inst✝ : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h✝² : ¬f a < f b
h✝¹ : ¬f a = f b
h✝ : a < b
⊢ False