harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem max_eq_eval_unapply :
    (Linear_CC' C hsC ho) ∘ (fun (l : MaxProducts C ho) ↦ Products.eval C l.val) =
    (fun l ↦ l.val.Tail.eval (C' C ho))

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ (⇑(Linear_CC' C hsC ho) ∘ fun l => Products.eval C ↑l) = fun l => Products.eval (C' C ho) (↑l).Tail

Tactic:
ext1 l

Result:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
⊢ (⇑(Linear_CC' C hsC ho) ∘ fun l => Products.eval C ↑l) l = Products.eval (C' C ho) (↑l).Tail

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : ↑(MaxProducts C ho)
⊢ (⇑(Linear_CC' C hsC ho) ∘ fun l => Products.eval C ↑l) l = Products.eval (C' C ho) (↑l).Tail

Tactic:
exact max_eq_eval _ _ _ _

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem scanl_head : (scanl f b v).head = b

Proof state:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
this : v = nil
⊢ (scanl f b v).head = b

Tactic:
simp only [this, scanl_nil, head_cons]

Result:
no goals

Proof state:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ (scanl f b v).head = b

Tactic:
have : v = nil := by simp only [eq_iff_true_of_subsingleton]

Result:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
this : v = nil
⊢ (scanl f b v).head = b

Proof state:
case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b (v.head ::ᵥ v.tail)).head = b

Tactic:
simp [← get_zero, get_eq_get_toList]

Result:
no goals

Proof state:
case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b

Tactic:
rw [← cons_head_tail v]

Result:
case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b (v.head ::ᵥ v.tail)).head = b

Proof state:
α : Type u_1
n : ℕ
β : Type u_6
f : β → α → β
b : β
v : Vector α n
⊢ (scanl f b v).head = b

Tactic:
cases n

Result:
case zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ (scanl f b v).head = b

case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b

Proof state:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 0
⊢ v = nil

Tactic:
simp only [eq_iff_true_of_subsingleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_udiv {x y : BitVec n} : (x / y).toFin = x.toFin / y.toFin

Proof state:
n : Nat
x y : BitVec n
⊢ (x / y).toFin = x.toFin / y.toFin

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Category/Grpd.lean
theorem piIsoPi_hom_π (J : Type u) (f : J → Grpd.{u, u}) (j : J) :
    (piIsoPi J f).hom ≫ Limits.Pi.π f j = CategoryTheory.Pi.eval _ j

Proof state:
J : Type u
f : J → Grpd
j : J
⊢ (piLimitFan f).π.app { as := j } = Pi.eval (fun i => ↑(f i)) j

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u
f : J → Grpd
j : J
⊢ (piIsoPi J f).hom ≫ Limits.Pi.π f j = Pi.eval (fun i => ↑(f i)) j

Tactic:
simp [piIsoPi]

Result:
J : Type u
f : J → Grpd
j : J
⊢ (piLimitFan f).π.app { as := j } = Pi.eval (fun i => ↑(f i)) j
-- Mathlib/Data/Real/EReal.lean
lemma sign_mul_inv_abs' (a : EReal) : (sign a) * ((a.abs⁻¹ : ℝ≥0∞) : EReal) = a⁻¹

Proof state:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
rw [sign_coe, _root_.sign_pos a_pos, SignType.coe_one, one_mul, abs_def a,
  ← ofReal_inv_of_pos (abs_pos_of_pos a_pos), coe_ennreal_ofReal,
    max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_inv a]

Result:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑|a|⁻¹ = ↑a⁻¹

Proof state:
case h_real
a : ℝ
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
rcases lt_trichotomy a 0 with (a_neg | rfl | a_pos)

Result:
case h_real.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

case h_real.inr.inl

⊢ ↑(sign ↑0) * ↑(↑0).abs⁻¹ = (↑0)⁻¹

case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Proof state:
case h_top

⊢ ↑(sign ⊤) * ↑⊤.abs⁻¹ = ⊤⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h_real.inr.inl

⊢ ↑(sign ↑0) * ↑(↑0).abs⁻¹ = (↑0)⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case h_real.inr.inr.e_a.e_a
a : ℝ
a_pos : 0 < a
⊢ |a| = a

Tactic:
exact abs_of_pos a_pos

Result:
no goals

Proof state:
case h_real.inr.inr
a : ℝ
a_pos : 0 < a
⊢ ↑|a|⁻¹ = ↑a⁻¹

Tactic:
congr

Result:
case h_real.inr.inr.e_a.e_a
a : ℝ
a_pos : 0 < a
⊢ |a| = a

Proof state:
case h_real.inl
a : ℝ
a_neg : a < 0
⊢ ↑(sign ↑a) * ↑(↑a).abs⁻¹ = (↑a)⁻¹

Tactic:
rw [sign_coe, _root_.sign_neg a_neg, coe_neg_one, neg_one_mul, abs_def a,
  ← ofReal_inv_of_pos (abs_pos_of_neg a_neg), coe_ennreal_ofReal,
  max_eq_left (inv_nonneg.2 (abs_nonneg a)), ← coe_neg |a|⁻¹, ← coe_inv a, abs_of_neg a_neg,
  ← _root_.inv_neg, neg_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem bind_eq_some : x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b

Proof state:
α✝¹ : Type u_1
b : α✝¹
α✝ : Type u_2
x : Option α✝
f : α✝ → Option α✝¹
⊢ x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem eq_ofRepr_eq_repr {b₁ b₂ : Basis ι R M} (h : ∀ x i, b₁.repr x i = b₂.repr x i) : b₁ = b₂ :=
  repr_injective <| by ext; apply h

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i
⊢ b₁.repr = b₂.repr

Tactic:
ext

Result:
case h.h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i
x✝ : M
a✝ : ι
⊢ (b₁.repr x✝) a✝ = (b₂.repr x✝) a✝

Proof state:
case h.h
ι : Type u_1
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b₁ b₂ : Basis ι R M
h : ∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i
x✝ : M
a✝ : ι
⊢ (b₁.repr x✝) a✝ = (b₂.repr x✝) a✝

Tactic:
apply h

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem finrank_comap (f : L →+* E) : finrank (A.comap f) L = relfinrank A f.fieldRange

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A : Subfield E
f : L →+* E
⊢ finrank (↥(comap f A)) L = A.relfinrank f.fieldRange

Tactic:
simpa using congr(toNat $(lift_rank_comap A f))

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem mem_sSup_of_directedOn {S : Set (Submonoid M)} (Sne : S.Nonempty)
    (hS : DirectedOn (· ≤ ·) S) {x : M} : x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
simp [sSup_eq_iSup', mem_iSup_of_directed hS.directed_val, SetCoe.exists, Subtype.coe_mk]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s

Tactic:
haveI : Nonempty S := Sne.to_subtype

Result:
M : Type u_1
inst✝ : MulOneClass M
S : Set (Submonoid M)
Sne : S.Nonempty
hS : DirectedOn (fun x1 x2 => x1 ≤ x2) S
x : M
this : Nonempty ↑S
⊢ x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[parity_simps] lemma odd_sub : Odd (m - n) ↔ (Odd m ↔ Even n)

Proof state:
m n : ℤ
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)

Tactic:
rw [← not_even_iff_odd, even_sub, not_iff, ← not_even_iff_odd]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem dropWhile_eq_drop_findIdx_not {xs : List α} {p : α → Bool} :
    dropWhile p xs = drop (xs.findIdx (fun a => !p a)) xs

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : dropWhile p xs = drop (findIdx (fun a => !p a) xs) xs
⊢ dropWhile p (x :: xs) = drop (findIdx (fun a => !p a) (x :: xs)) (x :: xs)

Tactic:
simp only [dropWhile_cons, ih, findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]

Result:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : dropWhile p xs = drop (findIdx (fun a => !p a) xs) xs
⊢ (if p x = true then drop (findIdx (fun a => !p a) xs) xs else x :: xs) =
    drop (if p x = false then 0 else findIdx (fun a => !p a) xs + 1) (x :: xs)

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ dropWhile p [] = drop (findIdx (fun a => !p a) []) []

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
xs : List α
ih : dropWhile p xs = drop (findIdx (fun a => !p a) xs) xs
⊢ (if p x = true then drop (findIdx (fun a => !p a) xs) xs else x :: xs) =
    drop (if p x = false then 0 else findIdx (fun a => !p a) xs + 1) (x :: xs)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
xs : List α
p : α → Bool
⊢ dropWhile p xs = drop (findIdx (fun a => !p a) xs) xs

Tactic:
induction xs with
| nil => simp
| cons x xs ih =>
  simp only [dropWhile_cons, ih, findIdx_cons, cond_eq_if, Bool.not_eq_eq_eq_not, Bool.not_true]
  split <;> simp_all

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.map_vadd_multiples [AddCommMonoid α] (hf : Periodic f c)
    (a : AddSubmonoid.multiples c) (x : α) : f (a +ᵥ x) = f x

Proof state:
case mk.intro
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
x : α
m : ℕ
⊢ f (⟨(fun i => i • c) m, ⋯⟩ +ᵥ x) = f x

Tactic:
simp [AddSubmonoid.vadd_def, add_comm _ x, hf.nsmul m x]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
a : ↥(AddSubmonoid.multiples c)
x : α
⊢ f (a +ᵥ x) = f x

Tactic:
rcases a with ⟨_, m, rfl⟩

Result:
case mk.intro
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
x : α
m : ℕ
⊢ f (⟨(fun i => i • c) m, ⋯⟩ +ᵥ x) = f x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem sub_ediv_of_dvd (a : Int) {b c : Int}
    (hcb : c ∣ b) : (a - b) / c = a / c - b / c

Proof state:
case e_a
a b c : Int
hcb : c ∣ b
⊢ -b / c = -(b / c)

Tactic:
exact Int.neg_ediv_of_dvd hcb

Result:
no goals

Proof state:
a b c : Int
hcb : c ∣ b
⊢ a / c + -b / c = a / c + -(b / c)

Tactic:
congr

Result:
case e_a
a b c : Int
hcb : c ∣ b
⊢ -b / c = -(b / c)

Proof state:
a b c : Int
hcb : c ∣ b
⊢ (a - b) / c = a / c - b / c

Tactic:
rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_ediv_of_dvd_right (Int.dvd_neg.2 hcb)]

Result:
a b c : Int
hcb : c ∣ b
⊢ a / c + -b / c = a / c + -(b / c)
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem extract.go₁_append_right : ∀ (s t : List Char) (i b : Nat) (e : Pos),
    b = utf8Len s + i → go₁ (s ++ t) ⟨i⟩ ⟨b⟩ e = go₂ t ⟨b⟩ e
| [], t, i, _, e, rfl => by cases t <;> simp [go₁, go₂]
| c :: cs, t, i, _, e, rfl => by
  simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.cons_append,
    Pos.addChar_eq]
  apply go₁_append_right; rw [Nat.add_right_comm, Nat.add_assoc]

Proof state:
c : Char
cs t : List Char
i : Nat
e : Pos
⊢ go₁ (c :: cs ++ t) { byteIdx := i } { byteIdx := utf8Len (c :: cs) + i } e =
    go₂ t { byteIdx := utf8Len (c :: cs) + i } e

Tactic:
simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.cons_append,
  Pos.addChar_eq]

Result:
c : Char
cs t : List Char
i : Nat
e : Pos
⊢ go₁ (cs ++ t) { byteIdx := i + c.utf8Size } { byteIdx := utf8Len cs + c.utf8Size + i } e =
    go₂ t { byteIdx := utf8Len cs + c.utf8Size + i } e

Proof state:
c : Char
cs t : List Char
i : Nat
e : Pos
⊢ go₁ (cs ++ t) { byteIdx := i + c.utf8Size } { byteIdx := utf8Len cs + c.utf8Size + i } e =
    go₂ t { byteIdx := utf8Len cs + c.utf8Size + i } e

Tactic:
apply go₁_append_right

Result:
case a
c : Char
cs t : List Char
i : Nat
e : Pos
⊢ utf8Len cs + c.utf8Size + i = utf8Len cs + (i + c.utf8Size)

Proof state:
t : List Char
i : Nat
e : Pos
⊢ go₁ ([] ++ t) { byteIdx := i } { byteIdx := utf8Len [] + i } e = go₂ t { byteIdx := utf8Len [] + i } e

Tactic:
cases t <;> simp [go₁, go₂]

Result:
no goals

Proof state:
case a
c : Char
cs t : List Char
i : Nat
e : Pos
⊢ utf8Len cs + c.utf8Size + i = utf8Len cs + (i + c.utf8Size)

Tactic:
rw [Nat.add_right_comm, Nat.add_assoc]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem lcm_cycleType (σ : Perm α) : σ.cycleType.lcm = orderOf σ

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType.lcm = orderOf σ

Tactic:
induction σ using cycle_induction_on with
| base_one => simp
| base_cycles σ hσ => simp [hσ.cycleType, hσ.orderOf]
| induction_disjoint σ τ hd _ hσ hτ => simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]

Result:
no goals

Proof state:
case base_one
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (cycleType 1).lcm = orderOf 1

Tactic:
simp

Result:
no goals

Proof state:
case induction_disjoint
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
hd : σ.Disjoint τ
a✝ : σ.IsCycle
hσ : σ.cycleType.lcm = orderOf σ
hτ : τ.cycleType.lcm = orderOf τ
⊢ (σ * τ).cycleType.lcm = orderOf (σ * τ)

Tactic:
simp [hd.cycleType, hd.orderOf, lcm_eq_nat_lcm, hσ, hτ]

Result:
no goals

Proof state:
case base_cycles
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ.IsCycle
⊢ σ.cycleType.lcm = orderOf σ

Tactic:
simp [hσ.cycleType, hσ.orderOf]

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_powerset_neg_one_pow_card_of_nonempty {α : Type*} {x : Finset α} (h0 : x.Nonempty) :
    (∑ m ∈ x.powerset, (-1 : ℤ) ^ #m) = 0

Proof state:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = 0

Tactic:
rw [sum_powerset_neg_one_pow_card]

Result:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ (if x = ∅ then 1 else 0) = 0

Proof state:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ (if x = ∅ then 1 else 0) = 0

Tactic:
exact if_neg (nonempty_iff_ne_empty.mp h0)

Result:
no goals

Proof state:
α : Type u_2
x : Finset α
h0 : x.Nonempty
⊢ ∑ m ∈ x.powerset, (-1) ^ #m = 0

Tactic:
classical
rw [sum_powerset_neg_one_pow_card]
exact if_neg (nonempty_iff_ne_empty.mp h0)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
/-- Note that this is not quite as useful as it looks because the measure takes values in `ℝ≥0∞`.
Thus the subtraction appearing is the truncated subtraction of `ℝ≥0∞`, rather than the
better-behaved subtraction of `ℝ`. -/
lemma prob_compl_eq_one_sub₀ (h : NullMeasurableSet s μ) : μ sᶜ = 1 - μ s

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝ : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
⊢ μ sᶜ = 1 - μ s

Tactic:
rw [measure_compl₀ h (measure_ne_top _ _), measure_univ]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma map_symm_eq_iff_eq_map {M : Sublattice β} {e : β ≃o α} :
    L.map ↑e.symm = M ↔ L = M.map ↑e

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M)

Tactic:
exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L = M ↔ L = map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M

Tactic:
simp_rw [← coe_inj]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
L : Sublattice α
M : Sublattice β
e : β ≃o α
⊢ ↑(map { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ } L) = ↑M ↔
    ↑L = ↑(map { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ } M)
-- Mathlib/NumberTheory/FunctionField.lean
theorem algebraMap_injective [Algebra Fq[X] F] [Algebra (RatFunc Fq) F]
    [IsScalarTower Fq[X] (RatFunc Fq) F] : Function.Injective (⇑(algebraMap Fq[X] F))

Proof state:
Fq : Type u_1
F : Type u_2
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ⇑(algebraMap Fq[X] F)

Tactic:
rw [IsScalarTower.algebraMap_eq Fq[X] (RatFunc Fq) F]

Result:
Fq : Type u_1
F : Type u_2
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ⇑((algebraMap (RatFunc Fq) F).comp (algebraMap Fq[X] (RatFunc Fq)))

Proof state:
Fq : Type u_1
F : Type u_2
inst✝⁴ : Field Fq
inst✝³ : Field F
inst✝² : Algebra Fq[X] F
inst✝¹ : Algebra (RatFunc Fq) F
inst✝ : IsScalarTower Fq[X] (RatFunc Fq) F
⊢ Function.Injective ⇑((algebraMap (RatFunc Fq) F).comp (algebraMap Fq[X] (RatFunc Fq)))

Tactic:
exact (algebraMap (RatFunc Fq) F).injective.comp (IsFractionRing.injective Fq[X] (RatFunc Fq))

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma finiteDimensionalOrder_iff_krullDim_ne_bot_and_top :
    FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Proof state:
case pos
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
simp [← not_infiniteDimensionalOrder_iff, ← krullDim_eq_top_iff]

Result:
no goals

Proof state:
case neg.mp
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
exact (fun h1 ↦ False.elim (h (LTSeries.nonempty_of_finiteDimensionalOrder α)))

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
constructor

Result:
case neg.mp
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α → krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

case neg.mpr
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Tactic:
by_cases h : Nonempty α

Result:
case pos
α : Type u_1
inst✝ : Preorder α
h : Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

case neg
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ FiniteDimensionalOrder α ↔ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤

Proof state:
case neg.mpr
α : Type u_1
inst✝ : Preorder α
h : ¬Nonempty α
⊢ krullDim α ≠ ⊥ ∧ krullDim α ≠ ⊤ → FiniteDimensionalOrder α

Tactic:
exact (fun h1 ↦ False.elim (h1.1 (krullDim_eq_bot_iff.mpr (not_nonempty_iff.mp h))))

Result:
no goals
-- Mathlib/Deprecated/Logic.lean
theorem let_eq {α : Sort v} {β : Sort u} {a₁ a₂ : α} {b₁ b₂ : α → β}
    (h₁ : a₁ = a₂) (h₂ : ∀ x, b₁ x = b₂ x) :
    (let x : α := a₁; b₁ x) = (let x : α := a₂; b₂ x)

Proof state:
α : Sort v
β : Sort u
a₁ a₂ : α
b₁ b₂ : α → β
h₁ : a₁ = a₂
h₂ : ∀ (x : α), b₁ x = b₂ x
⊢ (let x := a₁;
    b₁ x) =
    let x := a₂;
    b₂ x

Tactic:
simp [h₁, h₂]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem norm_sub_eq_add_norm_of_angle_eq_pi {x y : V} (h : angle x y = π) :
    ‖x - y‖ = ‖x‖ + ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x - y‖ = ‖x‖ + ‖y‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg (x - y)) (add_nonneg (norm_nonneg x) (norm_nonneg y)),
  norm_sub_pow_two_real, inner_eq_neg_mul_norm_of_angle_eq_pi h]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x‖ ^ 2 - 2 * -(‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π
⊢ ‖x‖ ^ 2 - 2 * -(‖x‖ * ‖y‖) + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_wf_aux : ∀ {x y : PSet.{u}}, Equiv x y → Acc (· ∈ ·) y
  | ⟨α, A⟩, ⟨β, B⟩, H =>
    ⟨_, by
      rintro ⟨γ, C⟩ ⟨b, hc⟩
      obtain ⟨a, ha⟩ := H.exists_right b
      have H := ha.trans hc.symm
      rw [mk_func] at H
      exact mem_wf_aux H⟩

Proof state:
case mk.intro.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H✝ : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
H : (A a).Equiv (mk γ C)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)

Tactic:
exact mem_wf_aux H

Result:
no goals

Proof state:
case mk.intro.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H✝ : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
H : ((mk α A).Func a).Equiv (mk γ C)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)

Tactic:
rw [mk_func] at H

Result:
case mk.intro.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H✝ : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
H : (A a).Equiv (mk γ C)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)

Proof state:
case mk.intro.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)

Tactic:
have H := ha.trans hc.symm

Result:
case mk.intro.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H✝ : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
H : ((mk α A).Func a).Equiv (mk γ C)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)

Proof state:
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
⊢ ∀ y ∈ mk β B, Acc (fun x1 x2 => x1 ∈ x2) y

Tactic:
rintro ⟨γ, C⟩ ⟨b, hc⟩

Result:
case mk.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)

Proof state:
case mk.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)

Tactic:
obtain ⟨a, ha⟩ := H.exists_right b

Result:
case mk.intro.intro
α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
γ : Type u
C : γ → PSet.{u}
b : (mk β B).Type
hc : (mk γ C).Equiv ((mk β B).Func b)
a : (mk α A).Type
ha : ((mk α A).Func a).Equiv ((mk β B).Func b)
⊢ Acc (fun x1 x2 => x1 ∈ x2) (mk γ C)