harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem cons_nil_iff_singleton {x b} : Red ((x, b) :: L) [] ↔ Red L [(x, not b)] :=
  Iff.intro
    (fun h => by
      have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h
      have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev
      let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂
      rw [singleton_iff] at h₁
      subst L'
      assumption)
    fun h => (cons_cons h).tail Step.cons_not

Proof state:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]

Tactic:
subst L'

Result:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]

Proof state:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
⊢ Red L [(x, !b)]

Tactic:
let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂

Result:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]

Proof state:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]

Tactic:
have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev

Result:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂ : Red ((x, !b) :: (x, b) :: L) L
⊢ Red L [(x, !b)]

Proof state:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
h₂ : Red L [(x, !b)]
⊢ Red L [(x, !b)]

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : Red [(x, !b)] L'
h₂ : Red L L'
⊢ Red L [(x, !b)]

Tactic:
rw [singleton_iff] at h₁

Result:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁✝ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
h₂✝ : Red ((x, !b) :: (x, b) :: L) L
L' : List (α × Bool)
h₁ : L' = [(x, !b)]
h₂ : Red L L'
⊢ Red L [(x, !b)]

Proof state:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
⊢ Red L [(x, !b)]

Tactic:
have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h

Result:
α : Type u
L : List (α × Bool)
x : α
b : Bool
h : Red ((x, b) :: L) []
h₁ : Red ((x, !b) :: (x, b) :: L) [(x, !b)]
⊢ Red L [(x, !b)]
-- Mathlib/Topology/ContinuousMap/Units.lean
theorem isUnit_iff_forall_isUnit (f : C(X, R)) : IsUnit f ↔ ∀ x, IsUnit (f x) :=
  Iff.intro (fun h => fun x => ⟨unitsLift.symm h.unit x, rfl⟩) fun h =>
    ⟨ContinuousMap.unitsLift (unitsOfForallIsUnit h), by ext; rfl⟩

Proof state:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
⊢ ↑(unitsLift (unitsOfForallIsUnit h)) = f

Tactic:
ext

Result:
case h
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
a✝ : X
⊢ ↑(unitsLift (unitsOfForallIsUnit h)) a✝ = f a✝

Proof state:
case h
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : NormedRing R
inst✝ : CompleteSpace R
f : C(X, R)
h : ∀ (x : X), IsUnit (f x)
a✝ : X
⊢ ↑(unitsLift (unitsOfForallIsUnit h)) a✝ = f a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Height.lean
theorem chainHeight_insert_of_forall_gt (a : α) (hx : ∀ b ∈ s, a < b) :
    (insert a s).chainHeight = s.chainHeight + 1

Proof state:
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
h' : y ∈ insert a s ∧ ys ∈ (insert a s).subchain ∧ ∀ b ∈ ys.head?, y < b
⊢ (y :: ys).length + 0 ≤ ys.length + 1

Tactic:
simp

Result:
no goals

Proof state:
case a.nil
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
h : [] ∈ (insert a s).subchain
⊢ ∃ l' ∈ s.subchain, [].length + 0 ≤ l'.length + 1

Tactic:
exact ⟨[], nil_mem_subchain _, zero_le _⟩

Result:
no goals

Proof state:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
h' : y ∈ insert a s ∧ ys ∈ (insert a s).subchain ∧ ∀ b ∈ ys.head?, y < b
i : α
hi : i ∈ ys
⊢ i ∈ s

Tactic:
apply (h'.2.1.2 i hi).resolve_left

Result:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
h' : y ∈ insert a s ∧ ys ∈ (insert a s).subchain ∧ ∀ b ∈ ys.head?, y < b
i : α
hi : i ∈ ys
⊢ ¬i = a

Proof state:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
⊢ ∃ l' ∈ s.subchain, (y :: ys).length + 0 ≤ l'.length + 1

Tactic:
have h' := cons_mem_subchain_iff.mp h

Result:
case a.cons
α : Type u_1
s : Set α
inst✝ : Preorder α
a : α
hx : ∀ b ∈ s, a < b
y : α
ys : List α
h : y :: ys ∈ (insert a s).subchain
h' : y ∈ insert a s ∧ ys ∈ (insert a s).subchain ∧ ∀ b ∈ ys.head?, y < b
⊢ ∃ l' ∈ s.subchain, (y :: ys).length + 0 ≤ l'.length + 1
-- Mathlib/Topology/MetricSpace/Kuratowski.lean
theorem embeddingOfSubset_isometry (H : DenseRange x) : Isometry (embeddingOfSubset x)

Proof state:
case intro
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e

Tactic:
have :=
  calc
    dist a b ≤ dist a (x n) + dist (x n) b := dist_triangle _ _ _
    _ = 2 * dist a (x n) + (dist b (x n) - dist a (x n)) := by simp [dist_comm]; ring
    _ ≤ 2 * dist a (x n) + |dist b (x n) - dist a (x n)| := by
      apply_rules [add_le_add_left, le_abs_self]
    _ ≤ 2 * (e / 2) + |embeddingOfSubset x b n - embeddingOfSubset x a n| := by
      rw [C]
      gcongr
    _ ≤ 2 * (e / 2) + dist (embeddingOfSubset x b) (embeddingOfSubset x a) := by
      gcongr
      simp only [dist_eq_norm]
      exact lp.norm_apply_le_norm ENNReal.top_ne_zero
        (embeddingOfSubset x b - embeddingOfSubset x a) n
    _ = dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e := by ring

Result:
case intro
α : Type u
inst✝ : MetricSpace α
x : ℕ → α
H : DenseRange x
a b : α
e : ℝ
epos : 0 < e
n : ℕ
hn : dist a (x n) < e / 2
C : dist b (x n) - dist a (x n) = ↑(embeddingOfSubset x b) n - ↑(embeddingOfSubset x a) n
this : dist a b ≤ dist (embeddingOfSubset x b) (embeddingOfSubset x a) + e
⊢ dist a b ≤ dist (embeddingOfSubset x a) (embeddingOfSubset x b) + e
-- Mathlib/Order/RelSeries.lean
lemma length_eq_zero (irrefl : Irreflexive r) : s.length = 0 ↔ {x | x ∈ s}.Subsingleton

Proof state:
α : Type u_1
r : Rel α α
s : RelSeries r
irrefl : Irreflexive r
⊢ s.length = 0 ↔ {x | x ∈ s}.Subsingleton

Tactic:
rw [← not_ne_iff, length_ne_zero irrefl, Set.not_nontrivial_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem dist_eq_iff_dist_orthogonalProjection_eq {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] {p₁ p₂ : P} (p₃ : P) (hp₁ : p₁ ∈ s) (hp₂ : p₂ ∈ s) :
    dist p₁ p₃ = dist p₂ p₃ ↔
      dist p₁ (orthogonalProjection s p₃) = dist p₂ (orthogonalProjection s p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ p₃ = dist p₂ p₃ ↔ dist p₁ ↑((orthogonalProjection s) p₃) = dist p₂ ↑((orthogonalProjection s) p₃)

Tactic:
rw [← mul_self_inj_of_nonneg dist_nonneg dist_nonneg, ←
  mul_self_inj_of_nonneg dist_nonneg dist_nonneg,
  dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₁,
  dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₃ hp₂]

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) +
        dist p₃ ↑((orthogonalProjection s) p₃) * dist p₃ ↑((orthogonalProjection s) p₃) =
      dist p₂ ↑((orthogonalProjection s) p₃) * dist p₂ ↑((orthogonalProjection s) p₃) +
        dist p₃ ↑((orthogonalProjection s) p₃) * dist p₃ ↑((orthogonalProjection s) p₃) ↔
    dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) =
      dist p₂ ↑((orthogonalProjection s) p₃) * dist p₂ ↑((orthogonalProjection s) p₃)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p₁ p₂ p₃ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) +
        dist p₃ ↑((orthogonalProjection s) p₃) * dist p₃ ↑((orthogonalProjection s) p₃) =
      dist p₂ ↑((orthogonalProjection s) p₃) * dist p₂ ↑((orthogonalProjection s) p₃) +
        dist p₃ ↑((orthogonalProjection s) p₃) * dist p₃ ↑((orthogonalProjection s) p₃) ↔
    dist p₁ ↑((orthogonalProjection s) p₃) * dist p₁ ↑((orthogonalProjection s) p₃) =
      dist p₂ ↑((orthogonalProjection s) p₃) * dist p₂ ↑((orthogonalProjection s) p₃)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_or_ne_mem_of_mem {a b : α} {l : Array α} (h' : a ∈ l.push b) :
    a = b ∨ (a ≠ b ∧ a ∈ l)

Proof state:
α : Type u_1
a b : α
l : Array α
h' : a ∈ l.push b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
if h : a = b then
  exact .inl h
else
  simp only [mem_push, h, or_false] at h'
  exact .inr ⟨h, h'⟩

Result:
no goals

Proof state:
α : Type u_1
a b : α
l : Array α
h : ¬a = b
h' : a ∈ l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact .inr ⟨h, h'⟩

Result:
no goals

Proof state:
α : Type u_1
a b : α
l : Array α
h' : a ∈ l.push b
h : ¬a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
simp only [mem_push, h, or_false] at h'

Result:
α : Type u_1
a b : α
l : Array α
h : ¬a = b
h' : a ∈ l
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Proof state:
α : Type u_1
a b : α
l : Array α
h' : a ∈ l.push b
h : a = b
⊢ a = b ∨ a ≠ b ∧ a ∈ l

Tactic:
exact .inl h

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
lemma takeUntil_cons {v' : V} {p : G.Walk v' v} (hwp : w ∈ p.support) (h : u ≠ w)
    (hadj : G.Adj u v') :
    (p.cons hadj).takeUntil w (List.mem_of_mem_tail hwp) = (p.takeUntil w hwp).cons hadj

Proof state:
V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
v' : V
p : G.Walk v' v
hwp : w ∈ p.support
h : u ≠ w
hadj : G.Adj u v'
⊢ (cons hadj p).takeUntil w ⋯ = cons hadj (p.takeUntil w hwp)

Tactic:
simp [Walk.takeUntil, h]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_one : s.ncard = 1 ↔ ∃ a, s = {a}

Proof state:
α : Type u_1
s : Set α
⊢ (∃ a, s = {a}) → s.ncard = 1

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
α : Type u_1
a : α
⊢ {a}.ncard = 1

Proof state:
α : Type u_1
s : Set α
h : s.ncard = 1
⊢ ∃ a, s = {a}

Tactic:
have hft := (finite_of_ncard_ne_zero (ne_zero_of_eq_one h)).fintype

Result:
α : Type u_1
s : Set α
h : s.ncard = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}

Proof state:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ ∀ (x : α), x ∈ s ↔ x = a

Tactic:
simp only [Finset.ext_iff, mem_toFinset, Finset.mem_singleton] at ha

Result:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a

Proof state:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
⊢ ∃ a, s = {a}

Tactic:
refine h.imp fun a ha ↦ ?_

Result:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ s = {a}

Proof state:
α : Type u_1
s : Set α
⊢ s.ncard = 1 ↔ ∃ a, s = {a}

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨a, rfl⟩; rw [ncard_singleton]⟩

Result:
α : Type u_1
s : Set α
h : s.ncard = 1
⊢ ∃ a, s = {a}

Proof state:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ s = {a}

Tactic:
simp_rw [Set.ext_iff, mem_singleton_iff]

Result:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : s.toFinset = {a}
⊢ ∀ (x : α), x ∈ s ↔ x = a

Proof state:
case intro
α : Type u_1
a : α
⊢ {a}.ncard = 1

Tactic:
rw [ncard_singleton]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
h : s.ncard = 1
hft : Fintype ↑s
⊢ ∃ a, s = {a}

Tactic:
simp_rw [ncard_eq_toFinset_card', @Finset.card_eq_one _ (toFinset s)] at h

Result:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
⊢ ∃ a, s = {a}

Proof state:
α : Type u_1
s : Set α
hft : Fintype ↑s
h : ∃ a, s.toFinset = {a}
a : α
ha : ∀ (a_1 : α), a_1 ∈ s ↔ a_1 = a
⊢ ∀ (x : α), x ∈ s ↔ x = a

Tactic:
exact ha

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem not_isUnit_X_pow_sub_one (R : Type*) [CommRing R] [Nontrivial R] (n : ℕ) :
    ¬IsUnit (X ^ n - 1 : R[X])

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
⊢ False

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : IsUnit (X ^ 0 - 1)
⊢ False

case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ False

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ False

Tactic:
apply hn

Result:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = 0

Proof state:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
hn : n ≠ 0
⊢ n = 0

Tactic:
rw [← @natDegree_one R, ← (monic_X_pow_sub_C _ hn).eq_one_of_isUnit h, natDegree_X_pow_sub_C]

Result:
no goals

Proof state:
case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
h : IsUnit (X ^ 0 - 1)
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
⊢ ¬IsUnit (X ^ n - 1)

Tactic:
intro h

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
n : ℕ
h : IsUnit (X ^ n - 1)
⊢ False
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma nnrpow_zero {a : A} : a ^ (0 : ℝ≥0) = 0

Proof state:
A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : NonUnitalRing A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : StarRing A
inst✝³ : Module ℝ A
inst✝² : SMulCommClass ℝ A A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
a : A
⊢ a ^ 0 = 0

Tactic:
simp [nnrpow_def, cfcₙ_apply_of_not_map_zero]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem map_comp_inr : (map fn fg h).comp inr = inr.comp fg

Proof state:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
⊢ (map fn fg h).comp inr = inr.comp fg

Tactic:
ext <;> simp [map]

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
lemma coe_eq_zero_iff_of_mem_Ico (ha : a ∈ Ico 0 p) :
    (a : AddCircle p) = 0 ↔ a = 0

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
⊢ 0 ∈ Ico 0 (0 + p)

Tactic:
simpa [zero_add, left_mem_Ico] using hp.out

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
⊢ ↑a = 0 ↔ a = 0

Tactic:
have h0 : 0 ∈ Ico 0 (0 + p) := by simpa [zero_add, left_mem_Ico] using hp.out

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ a = 0

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ a = 0

Tactic:
have ha' : a ∈ Ico 0 (0 + p) := by rwa [zero_add]

Result:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ a = 0

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ a ∈ Ico 0 (0 + p)

Tactic:
rwa [zero_add]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : LinearOrderedAddCommGroup 𝕜
p : 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
ha' : a ∈ Ico 0 (0 + p)
⊢ ↑a = 0 ↔ a = 0

Tactic:
rw [← AddCircle.coe_eq_coe_iff_of_mem_Ico ha' h0, QuotientAddGroup.mk_zero]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
theorem prodComparison_inv_natural (f : A ⟶ A') (g : B ⟶ B') [IsIso (prodComparison F A' B')] :
    inv (prodComparison F A B) ≫ F.map (f ⊗ g) =
      (F.map f ⊗ F.map g) ≫ inv (prodComparison F A' B')

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ChosenFiniteProducts C
D : Type u₁
inst✝³ : Category.{v₁, u₁} D
inst✝² : ChosenFiniteProducts D
F : C ⥤ D
A B A' B' : C
inst✝¹ : IsIso (prodComparison F A B)
f : A ⟶ A'
g : B ⟶ B'
inst✝ : IsIso (prodComparison F A' B')
⊢ inv (prodComparison F A B) ≫ F.map (f ⊗ g) = (F.map f ⊗ F.map g) ≫ inv (prodComparison F A' B')

Tactic:
rw [IsIso.eq_comp_inv, Category.assoc, IsIso.inv_comp_eq, prodComparison_natural]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem LpAddConst_lt_top (p : ℝ≥0∞) : LpAddConst p < ∞

Proof state:
p : ℝ≥0∞
⊢ LpAddConst p < ⊤

Tactic:
rw [LpAddConst]

Result:
p : ℝ≥0∞
⊢ (if p ∈ Set.Ioo 0 1 then 2 ^ (1 / p.toReal - 1) else 1) < ⊤

Proof state:
p : ℝ≥0∞
⊢ (if p ∈ Set.Ioo 0 1 then 2 ^ (1 / p.toReal - 1) else 1) < ⊤

Tactic:
split_ifs with h

Result:
case pos
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / p.toReal - 1) < ⊤

case neg
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ 1 < ⊤

Proof state:
case neg
p : ℝ≥0∞
h : p ∉ Set.Ioo 0 1
⊢ 1 < ⊤

Tactic:
exact ENNReal.one_lt_top

Result:
no goals

Proof state:
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ ENNReal.toReal 1 ≤ p⁻¹.toReal

Tactic:
exact ENNReal.toReal_mono (by simpa using h.1.ne') (ENNReal.one_le_inv.2 h.2.le)

Result:
no goals

Proof state:
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 0 ≤ 1 / p.toReal - 1

Tactic:
rw [one_div, sub_nonneg, ← ENNReal.toReal_inv, ← ENNReal.one_toReal]

Result:
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ ENNReal.toReal 1 ≤ p⁻¹.toReal

Proof state:
case pos
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 2 ^ (1 / p.toReal - 1) < ⊤

Tactic:
apply ENNReal.rpow_lt_top_of_nonneg _ ENNReal.ofNat_ne_top

Result:
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ 0 ≤ 1 / p.toReal - 1

Proof state:
p : ℝ≥0∞
h : p ∈ Set.Ioo 0 1
⊢ p⁻¹ ≠ ⊤

Tactic:
simpa using h.1.ne'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertManyIfNewUnit_empty_list_nil :
    insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) ([] : List α) =
      (empty : Raw₀ α (fun _ => Unit))

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
⊢ (insertManyIfNewUnit empty []).val = empty

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem orientation_neg_single (e : Basis ι R M) (i : ι) :
    (e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
i : ι
⊢ (e.unitsSMul (Function.update 1 i (-1))).orientation = -e.orientation

Tactic:
rw [orientation_unitsSMul, Finset.prod_update_of_mem (Finset.mem_univ _)]

Result:
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
i : ι
⊢ (-1 * ∏ x ∈ Finset.univ \ {i}, 1 x)⁻¹ • e.orientation = -e.orientation

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedCommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e : Basis ι R M
i : ι
⊢ (-1 * ∏ x ∈ Finset.univ \ {i}, 1 x)⁻¹ • e.orientation = -e.orientation

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Rat/Cast/Defs.lean
@[norm_cast]
lemma cast_div_of_ne_zero (hq : (q.den : α) ≠ 0) (hr : (r.num : α) ≠ 0) :
    ↑(q / r) = (q / r : α)

Proof state:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0

Tactic:
push_cast

Result:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.den * ↑r.num ≠ 0

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q / r) = ↑q / ↑r

Tactic:
rw [div_def, cast_divNat_of_ne_zero, cast_def, cast_def, div_eq_mul_inv (_ / _),
  inv_div, (Nat.commute_cast _ _).div_mul_div_comm (Nat.commute_cast _ _)]

Result:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.den * r.num) ≠ 0

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑(q.num * r.den) / ↑(q.den * r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

Tactic:
push_cast

Result:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.num * ↑r.den / (↑q.den * ↑r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

Proof state:
case hb
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.den * ↑r.num ≠ 0

Tactic:
exact mul_ne_zero hq hr

Result:
no goals

Proof state:
α : Type u_3
inst✝ : DivisionSemiring α
q r : ℚ≥0
hq : ↑q.den ≠ 0
hr : ↑r.num ≠ 0
⊢ ↑q.num * ↑r.den / (↑q.den * ↑r.num) = ↑q.num * ↑r.den / (↑q.den * ↑r.num)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem map_X (s : σ) : map σ f (X s) = X s

Proof state:
σ : Type u_1
R : Type u_2
S : Type u_3
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
s : σ
⊢ (map σ f) (X s) = X s

Tactic:
simp [MvPowerSeries.X]

Result:
no goals