mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.Translate.GuessName

Goal state before:
pp: x : String
s : List String
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (s.length + [].length, s.length)
    ([].length + (x :: s).length, [].length)

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.Translate.GuessName

Goal state before:
pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : (pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂)
    ((List.drop 1 (s' ++ [pre]) ++ l).length + [].length, (List.drop 1 (s' ++ [pre]) ++ l).length)
    ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.Translate.GuessName

Goal state before:
pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (l.length + [].length, l.length)
    ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.Translate.GuessName

Goal state before:
pp: pre : String
l s' : List String
s : List String := s' ++ [pre]
t : String := String.join s
h✝ : ¬(pre == "_" && (String.Pos.Raw.get t 0).isUpper) = true
⊢ Prod.Lex (fun a₁ a₂ ↦ a₁ < a₂) (fun a₁ a₂ ↦ a₁ < a₂) (l.length + (s' ++ [pre]).length, l.length)
    ((pre :: l).length + s'.length, (pre :: l).length)

Tactic:
grind

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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a * b h✝ = a * b h✝

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a * c h✝ = a * c h✝

Tactic:
rfl

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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ * c = a h✝ * c

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ * c = b h✝ * c

Tactic:
rfl

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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ * c h✝ = a h✝ * c h✝

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ * d h✝ = b h✝ * d h✝

Tactic:
rfl

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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : P
⊢ a * c = a * c

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : ¬P
⊢ b * d = b * d

Tactic:
rfl

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

Goal state before:
pp: case isTrue
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : P
⊢ -b = -b

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : ¬P
⊢ -c = -c

Tactic:
rfl

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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a / b h✝ = a / b h✝

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a / c h✝ = a / c h✝

Tactic:
rfl

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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ / c = a h✝ / c

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ / c = b h✝ / c

Tactic:
rfl

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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ / c h✝ = a h✝ / c h✝

Tactic:
rfl

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

Goal state before:
pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ / d h✝ = b h✝ / d h✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: r✝ r : ArgReorder
n : Nat
cycle : { l // 2 ≤ l.length }
⊢ cycle.val ≠ []

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: n : Nat
map✝¹ : Vector (Option (Fin n)) n
map✝ : Vector (Option (Fin n)) n := map✝¹
perm✝ : List { l // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
__r✝² : Option Permutation := __s✝¹.fst
__s✝ : Vector (Option (Fin n)) n × List { l // 2 ≤ l.length } := __s✝¹.snd
map : Vector (Option (Fin n)) n := __s✝.fst
perm : List { l // 2 ≤ l.length } := __s✝.snd
j✝ : Fin n
j : Fin n := j✝
__r✝ : Unit
⊢ 2 ≤ [i, ↑j].length

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.Translate.Reorder

Goal state before:
pp: n : Nat
map✝³ : Vector (Option (Fin n)) n
map✝² : Vector (Option (Fin n)) n := map✝³
perm✝ : List { l // 2 ≤ l.length } := []
i : Nat
h : i ∈ *...n
__r✝⁷ : Option Permutation := __s✝⁴.fst
__s✝³ : Vector (Option (Fin n)) n × List { l // 2 ≤ l.length } := __s✝⁴.snd
map✝¹ : Vector (Option (Fin n)) n := __s✝³.fst
perm : List { l // 2 ≤ l.length } := __s✝³.snd
j✝² : Fin n
j✝¹ : Fin n := j✝²
__r✝⁵ : Unit
cycle✝ : { l // 2 ≤ l.length } := ⟨[i, ↑j✝¹], ⋯⟩
x✝ : Unit
__r✝³ : Option Permutation := __s✝².fst
__s✝¹ : Vector (Option (Fin n)) n × Fin n × { l // 2 ≤ l.length } := __s✝².snd
map✝ : Vector (Option (Fin n)) n := __s✝¹.fst
__s✝ : Fin n × { l // 2 ≤ l.length } := __s✝¹.snd
j✝ : Fin n := __s✝.fst
cycle : { l // 2 ≤ l.length } := __s✝.snd
j' : Fin n
map : Vector (Option (Fin n)) n := map✝.set! (↑j✝) none
__r✝¹ : Unit
j : Fin n := j'
⊢ 2 ≤ (cycle.val ++ [↑j]).length

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case false
n : Nat
⊢ bit false n = 2 * n + false.toNat

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case true
n : Nat
⊢ bit true n = 2 * n + true.toNat

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
h : (b : Bool) → (n : Nat) → motive (bit b n)
b : Bool
n : Nat
e✝ : motive (bit b n) = motive (bit b n)
⊢ e✝ ▸ h b n = h b n

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
b : Bool
n : Nat
h : bit false 0 zero = zero ∨ (n = 0 → b = true)
h' : ¬Nat.bit b n = 0
e✝ : motive (Nat.bit b n) = motive (Nat.bit b n)
⊢ e✝ ▸ bit b n (binaryRec zero bit n) = bit b n (binaryRec zero bit n)

Tactic:
rfl

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

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ SemiconjBy (a * b) x z

Tactic:
unfold SemiconjBy
  rw [mul_assoc, hb.eq, ← mul_assoc, ha.eq, mul_assoc]

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

Goal state before:
pp: case refl
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ } =
    { one := one₁, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 0 → npowRec' (2 * m_1) m = npowRec' m_1 (m * m)
⊢ npowRec' (2 * 0) m = npowRec' 0 (m * m)

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
m : M
k' : ℕ
ih : ∀ (m_1 : ℕ), m_1 < 0 → npowRec (m_1 + 1) m = 1 * npowRec' (m_1 + 1) m
⊢ npowRec (0 + 1) m = 1 * npowRec' (0 + 1) m

Tactic:
rfl

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

Goal state before:
pp: M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
n : ℕ
m : M
⊢ npowRecAuto (n + 1) m = npowRecAuto n m * m

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : p x
h : ∀ (y : α), y ∈ xs → p y → x = y
⊢ (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) x ∧ ∀ (y : α), (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = x

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : p x
x✝ : ∃! x_1, x_1 ∈ x :: xs ∧ p x_1
y : α
hy : y ∈ xs
hp : p y
z : α
h : (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) z ∧ ∀ (y : α), (fun x_1 ↦ x_1 ∈ x :: xs ∧ p x_1) y → y = z
⊢ z = y

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α✝ : Sort u_1
α : Type u_2
inst✝¹ : DecidableEq α
p : α → Prop
inst✝ : DecidablePred p
x : α
xs : List α
hx : ¬p x
this : Decidable (∃! x, x ∈ xs ∧ p x)
⊢ (∃! x, x ∈ xs ∧ p x) ↔ ∃! x_1, x_1 ∈ x :: xs ∧ p x_1

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Nontrivial α
inst✝ : DecidableEq α
x : α
⊢ ∃ y, y ≠ x

Tactic:
rcases exists_pair_ne α with ⟨y, y', h⟩
  by_cases hx : x = y
  · rw [← hx] at h
    exact ⟨y', h.symm⟩
  · exact ⟨y, Ne.symm hx⟩

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl
α : Sort u_1
inst✝ : Subsingleton α
p : α → Prop
x✝¹ x✝ : Subtype p
x : α
property✝¹ property✝ : p x
⊢ ⟨x, property✝¹⟩ = ⟨x, property✝⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl.refl
α : Sort u_2
γ : Sort u_3
f : α → γ
x : α
⊢ f x = f x

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl.refl.refl
α₁ : Sort u
β₁ : α₁ → Sort v
f₁ : (a : α₁) → β₁ a
a₁ : α₁
ht : ∀ (t₁ t₂ : α₁), t₁ ≍ t₂ → β₁ t₁ = β₁ t₂
hf : α₁ = α₁ → β₁ ≍ β₁ → f₁ ≍ f₁
⊢ f₁ a₁ ≍ f₁ a₁

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ⊢ Xor True = Not

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: ⊢ Xor False = id

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a b = Xor b a

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a : Prop
⊢ Xor a a = False

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor (¬a) b ↔ (a ↔ b)

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor a ¬b ↔ (a ↔ b)

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
⊢ Xor (¬a) ¬b ↔ Xor a b

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: a b : Prop
h : Xor a b
⊢ a ∨ b

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α γ : Sort u_1
a : α
c : γ
⊢ cast ⋯ a ≍ c ↔ a ≍ c

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α β : Sort u_1
a : α
b : β
⊢ a ≍ cast ⋯ b ↔ a ≍ b

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case refl
α : Sort u
a : α
e : α = α
⊢ a = cast e a

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
p : α → Prop
b : Prop
ha : Nonempty α
⊢ (∀ (x : α), p x) → b ↔ ∃ x, p x → b

Tactic:
by
  classical
  let ⟨a⟩ := ha
  refine ⟨fun h ↦ not_forall_not.1 fun h' ↦ ?_, fun ⟨x, hx⟩ h ↦ hx (h x)⟩
  exact if hb : b then h' a fun _ ↦ hb else hb <| h fun x ↦ (Classical.not_imp.1 (h' x)).1

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : Prop
inst✝ : Decidable P
a : α
B : ¬P → α
⊢ dite P (fun x ↦ a) B ≠ a ↔ ∃ h, a ≠ B h

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
x y : α
z : β
⊢ f (if P then x else y) z = if P then f x z else f y z

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
⊢ (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
by
  by_cases p : P <;> simp [p]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
by
  by_cases p : P <;> simp [p]

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inl.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : p y
⊢ x = y

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inl.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : p x
hy : ¬p y
⊢ x = y

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inr.inl
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : p y
⊢ x = y

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Basic

Goal state before:
pp: case inr.inr
α : Sort u_3
β : Sort u_4
p : β → Prop
inst✝ : DecidablePred p
g : β → α
hg : Injective g
f : β → α
hf : Injective f
h : ∀ (x y : β), g x = f y → x = y
x y : β
x✝ : (fun x ↦ if p x then g x else f x) x = (fun x ↦ if p x then g x else f x) y
hx : ¬p x
hy : ¬p y
⊢ x = y

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Unique

Goal state before:
pp: α : Sort u_1
inst✝ : Unique α
β : α → Sort v
f : (a : α) → β a
i x✝¹ : α
x✝ : i ≍ x✝¹
⊢ f default ≍ Function.const α (f default) x✝¹

Tactic:
rfl

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

Goal state before:
pp: α : Sort u
β : α → Sort v
f f' : (a : α) → β a
h : ∀ (a a' : α), a ≍ a' → f a ≍ f' a'
this : ∀ (a : α), f a ≍ f' a
⊢ f ≍ f'

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
p : α → Prop
inst✝ : DecidablePred p
f : { a // p a } → β
f' : { a // ¬p a } → β
hf : Injective f
hf' : Injective f'
im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩
x₁ x₂ : α
h : (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₁ = (fun x ↦ if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩) x₂
⊢ x₁ = x₂

Tactic:
grind

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

Goal state before:
pp: α : Sort u
inst✝ : DecidableEq α
β : Sort u_1
f₁ : α → β
a'₁ : α
v₁ : β
a₁ : α
⊢ update f₁ a'₁ v₁ a₁ = update f₁ a'₁ v₁ a₁

Tactic:
rfl

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

Goal state before:
pp: ι : Sort u_1
κ : Sort u_2
α : κ → Sort u_3
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
ctor : ι → κ
x✝ : Injective ctor
recursor : ((i : ι) → α (ctor i)) → (i : κ) → α i
h : ∀ (f : (i : ι) → α (ctor i)) (i : ι), recursor f (ctor i) = f i
h2 : ∀ (f₁ f₂ : (i : ι) → α (ctor i)) (k : κ), (∀ (i : ι), ctor i ≠ k) → recursor f₁ k = recursor f₂ k
f : (i : ι) → α (ctor i)
i : ι
x : α (ctor i)
⊢ recursor (update f i x) = update (recursor f) (ctor i) x

Tactic:
grind

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

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
f : (i : ι) → α i → β i
g : (i : ι) → α i
i : ι
v : α i
j : ι
⊢ f j (update g i v j) = update (fun k ↦ f k (g k)) i (f i v) j

Tactic:
grind

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

Goal state before:
pp: ι : Sort u_1
inst✝ : DecidableEq ι
α : ι → Sort u_2
β : ι → Sort u_3
γ : ι → Sort u_4
f : (i : ι) → α i → β i → γ i
g : (i : ι) → α i
h : (i : ι) → β i
i : ι
v : α i
w : β i
j : ι
⊢ f j (update g i v j) (update h i w j) = update (fun k ↦ f k (g k) (h k)) i (f i v w) j

Tactic:
grind

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

Goal state before:
pp: α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
P : ⦃a : α⦄ → β a → Prop
f : (a : α) → β a
a' : α
v : β a'
a : α
⊢ P (update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)

Tactic:
grind

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

Goal state before:
pp: α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a b : α
h : a ≠ b
v : β a
w : β b
f : (a : α) → β a
⊢ update (update f a v) b w = update (update f b w) a v

Tactic:
grind

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

Goal state before:
pp: α : Sort u_2
inst✝ : DecidableEq α
β : α → Sort u_1
a : α
v w : β a
f : (a : α) → β a
⊢ update (update f a v) a w = update f a w

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g ↦ extend f g e') g₁ = (fun g ↦ extend f g e') g₂
x : α
⊢ g₁ x = g₂ x

Tactic:
have H := congr_fun hg (f x)

Goal state after:
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β
hf : Injective f
e' : β → γ
g₁ g₂ : α → γ
hg : (fun g ↦ extend f g e') g₁ = (fun g ↦ extend f g e') g₂
x : α
H : (fun g ↦ extend f g e') g₁ (f x) = (fun g ↦ extend f g e') g₂ (f x)
⊢ g₁ x = g₂ x
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
γ : β → Sort v
f : α → β
g : β → α
h : LeftInverse g f
C : (a : α) → γ (f a)
a : α
⊢ cast ⋯ (C (g (f a))) = C a

Tactic:
grind

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

Goal state before:
pp: case refl
F : Sort u_1
α : Sort u_2
β : α → Sort u_3
i : DFunLike F α β
f : F
⊢ ⇑f = ⇑f

Tactic:
rfl

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

Goal state before:
pp: case pos
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : P
⊢ (f h✝) x = (f h✝) x

Tactic:
rfl

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

Goal state before:
pp: case neg
F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
h✝ : ¬P
⊢ (g h✝) x = (g h✝) x

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r p : α → α → Prop
hp : r ≤ p
a : α
⊢ ReflGen p a a

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r : α → α → Prop
a b c : α
inst✝ : Std.Symm r
x y : α
⊢ ReflTransGen r x x

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p q : α → Prop
h : ∀ (x : α), p x ↔ q x
a1 : { x // p x }
a2 : { x // q x }
⊢ ∀ (a2' : { x // p x }), a1 ≍ a2' ↔ ↑a1 = ↑a2'

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α β : Sort u_4
p : α → Prop
q : β → Prop
a : { x // p x }
b : { y // q y }
h : α = β
h' : p ≍ q
⊢ a ≍ b ↔ ↑a ≍ ↑b

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : { a // p a }
b : α
⊢ ↑a = b ↔ ∃ h, a = ⟨b, h⟩

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_1
p : α → Prop
a : Subtype p
b : α
⊢ (∃ h, ⟨b, h⟩ = a) ↔ b = ↑a

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
a b : α
⊢ b = b ∨ ∃ c, r b c ∧ ReflTransGen r c b

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case head
α : Type u_1
r : α → α → Prop
a b a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : ReflTransGen r c✝ b
a✝ : c✝ = b ∨ ∃ c, r c✝ c ∧ ReflTransGen r c b
⊢ a✝¹ = b ∨ ∃ c, r a✝¹ c ∧ ReflTransGen r c b

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
f : (x : α) → β x
p : α → Prop
x : Subtype p
⊢ restrict p f x = f ↑x

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Subtype

Goal state before:
pp: α : Sort u_5
β : α → Type u_4
ne : ∀ (a : α), Nonempty (β a)
p : α → Prop
f : (x : Subtype p) → β ↑x
⊢ ((fun f ↦ restrict p f) fun x ↦ if h : p x then f ⟨x, h⟩ else ⋯.some) = f

Tactic:
grind

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr.inl
α : Type u_1
r : α → α → Prop
a : α
⊢ ReflTransGen r a a

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c : α
hac : r a c
⊢ ReflTransGen r a a

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a c b✝ : α
hac : r a b✝
⊢ ReflTransGen r b✝ b✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2.inl
α : Type u_1
r : α → α → Prop
b : α
⊢ ReflTransGen r b b

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refl
α : Type u_1
r : α → α → Prop
i✝¹ i✝ : α
⊢ ReflTransGen (Function.swap r) i✝ i✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ TransGen (ReflGen r) = ReflTransGen r

Tactic:
ext x y
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simpa [reflTransGen_eq_self] using h.mono reflGen_le_reflTransGen x y |>.to_reflTransGen
  · obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
    · exact .single .refl
    · exact h.mono (fun _ _ ↦ .single) x y

Goal state after:
Module: Mathlib.Data.Quot

Goal state before:
pp: α : Sort u_3
r : α → α → Prop
iseqv✝¹ iseqv✝ : Equivalence r
Eq : ∀ (a b : α), { r := r, iseqv := iseqv✝¹ } a b ↔ { r := r, iseqv := iseqv✝ } a b
⊢ { r := r, iseqv := iseqv✝¹ } = { r := r, iseqv := iseqv✝ }

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: α : Type u
f : α → α
m n : ℕ
x : α
⊢ (f^[m] ∘ f^[n]) x = f^[m] (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.7
h : α = β
⊢ LeftInverse (cast ⋯) (cast h)

Tactic:
grind

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

Goal state before:
pp: α✝ : Sort u
β✝ : Sort v
γ : Sort w
α β : Sort ?u.7
h : α = β
⊢ RightInverse (cast ⋯) (cast h)

Tactic:
grind

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

Goal state before:
pp: α : Sort u_1
x : α
⊢ (Equiv.cast ⋯) x = ((Equiv.cast ⋯).trans (Equiv.cast ⋯)) x

Tactic:
rfl

Goal state after: