harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Condexp.lean
theorem _root_.MeasureTheory.Integrable.integral_norm_condExpKernel (hf_int : Integrable f μ) :
    Integrable (fun ω => ∫ y, ‖f y‖ ∂condExpKernel μ m ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂(condExpKernel μ m) ω) μ

Tactic:
rw [condExpKernel_eq]

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂((condDistrib id id μ).comap id ⋯) ω) μ

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂((condDistrib id id μ).comap id ⋯) ω) μ

Tactic:
convert Integrable.integral_norm_condDistrib
  (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
  (hf_int.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ)) using 1

Result:
no goals

Proof state:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
⊢ Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂(condExpKernel μ m) ω) μ

Tactic:
nontriviality Ω

Result:
Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : NormedAddCommGroup F
f : Ω → F
hf_int : Integrable f μ
a✝ : Nontrivial Ω
⊢ Integrable (fun ω => ∫ (y : Ω), ‖f y‖ ∂(condExpKernel μ m) ω) μ
-- Mathlib/.lake/packages/batteries/Batteries/Data/Stream.lean
theorem fst_take_succ [Stream σ α] (s : σ) :
    (take s (n+1)).fst = match next? s with
      | none => []
      | some (a, s) => a :: (take s n).fst

Proof state:
σ : Type u_1
α : Type u_2
n : Nat
inst✝ : Stream σ α
s : σ
⊢ (match next? s with
      | none => ([], s)
      | some (a, s) => (a :: (take s n).fst, (take s n).snd)).fst =
    match next? s with
    | none => []
    | some (a, s) => a :: (take s n).fst

Tactic:
split <;> rfl

Result:
no goals

Proof state:
σ : Type u_1
α : Type u_2
n : Nat
inst✝ : Stream σ α
s : σ
⊢ (take s (n + 1)).fst =
    match next? s with
    | none => []
    | some (a, s) => a :: (take s n).fst

Tactic:
simp only [take]

Result:
σ : Type u_1
α : Type u_2
n : Nat
inst✝ : Stream σ α
s : σ
⊢ (match next? s with
      | none => ([], s)
      | some (a, s) => (a :: (take s n).fst, (take s n).snd)).fst =
    match next? s with
    | none => []
    | some (a, s) => a :: (take s n).fst
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocMod_sub_zsmul' (a b : α) (m : ℤ) :
    toIocMod hp (a - m • p) b = toIocMod hp a b - m • p

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a - m • p) b = toIocMod hp a b - m • p

Tactic:
simp_rw [sub_eq_add_neg, ← neg_smul, toIocMod_add_zsmul']

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_nsmul (m : ℕ) (x : 𝕎 R) : truncateFun n (m • x) = m • truncateFun n x

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
x : 𝕎 R
⊢ truncateFun n (m • x) = m • truncateFun n x

Tactic:
witt_truncateFun_tac

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
lemma eq_zero_of_isNilpotent_isSemisimple (hn : IsNilpotent f) (hs : f.IsSemisimple) : f = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ annihilator R[X] (AEval R M f)
⊢ X ∈ annihilator R[X] (AEval R M f)

Tactic:
exact hs.annihilator_isRadical _ _ ⟨n, h0⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ f = 0

Tactic:
rw [← aeval_X (R := R) f]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ (aeval f) X = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : (aeval f) (X ^ n) = 0
⊢ (aeval f) X = 0

Tactic:
rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M)] at h0 ⊢

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : X ^ n ∈ annihilator R[X] (AEval R M f)
⊢ X ∈ annihilator R[X] (AEval R M f)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ (aeval f) X = 0

Tactic:
rw [← aeval_X_pow (R := R) f] at h0

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : (aeval f) (X ^ n) = 0
⊢ (aeval f) X = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
⊢ f = 0

Tactic:
have ⟨n, h0⟩ := hn

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
hn : IsNilpotent f
hs : f.IsSemisimple
n : ℕ
h0 : f ^ n = 0
⊢ f = 0
-- Mathlib/Data/QPF/Univariate/Basic.lean
theorem id_map {α : Type _} (x : F α) : id <$> x = x

Proof state:
case mk
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ id <$> abs ⟨a, f⟩ = abs ⟨a, f⟩

Tactic:
rw [← abs_map]

Result:
case mk
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ abs ((P F).map id ⟨a, f⟩) = abs ⟨a, f⟩

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ id <$> x = x

Tactic:
rw [← abs_repr x]

Result:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ id <$> abs (repr x) = abs (repr x)

Proof state:
case mk
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ abs ((P F).map id ⟨a, f⟩) = abs ⟨a, f⟩

Tactic:
rfl

Result:
no goals

Proof state:
F : Type u → Type u
q : QPF F
α : Type u
x : F α
⊢ id <$> abs (repr x) = abs (repr x)

Tactic:
obtain ⟨a, f⟩ := repr x

Result:
case mk
F : Type u → Type u
q : QPF F
α : Type u
x : F α
a : (P F).A
f : (P F).B a → α
⊢ id <$> abs ⟨a, f⟩ = abs ⟨a, f⟩
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_alter_self {k : α} {fallback : β} (h : m.1.WF) {f : Option β → Option β} :
    Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
k : α
fallback : β
h : m.val.WF
f : Option β → Option β
⊢ getD (alter m k f) k fallback = (f (get? m k)).getD fallback

Tactic:
simp only [h, getD_alter, BEq.refl, reduceIte]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get?_range' (s step) {m n : Nat} (h : m < n) :
    get? (range' s n step) m = some (s + step * m)

Proof state:
s step m n : Nat
h : m < n
⊢ (range' s n step).get? m = some (s + step * m)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.lt_irrefl (a : BitVec n) : (BitVec.ult a a) = false

Proof state:
n : Nat
a : BitVec n
⊢ a.ult a = false

Tactic:
rw [← Bool.not_eq_true, ← BitVec.lt_ult]

Result:
n : Nat
a : BitVec n
⊢ ¬a < a

Proof state:
n : Nat
a : BitVec n
⊢ ¬a < a

Tactic:
exact _root_.BitVec.lt_irrefl _

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
theorem mem_pow {a : α} {n : ℕ} :
    a ∈ s ^ n ↔ ∃ f : Fin n → s, (List.ofFn fun i => ↑(f i)).prod = a

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
a : α
n : ℕ
⊢ a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a

Tactic:
simp [← mem_coe, coe_pow, Set.mem_pow]

Result:
no goals
-- Mathlib/Data/Matrix/Invertible.lean
theorem invOf_add_mul_mul [Invertible (A + U*C*V)] :
    ⅟(A + U*C*V) = ⅟A - ⅟A*U*⅟(⅟C + V*⅟A*U)*V*⅟A

Proof state:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝³ : Invertible A
inst✝² : Invertible C
inst✝¹ : Invertible (⅟C + V * ⅟A * U)
inst✝ : Invertible (A + U * C * V)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul U C V
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
convert (rfl : ⅟(A + U*C*V) = _)

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝³ : Invertible A
inst✝² : Invertible C
inst✝¹ : Invertible (⅟C + V * ⅟A * U)
inst✝ : Invertible (A + U * C * V)
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A

Tactic:
letI := invertibleAddMulMul A U C V

Result:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁸ : Fintype n
inst✝⁷ : DecidableEq n
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝³ : Invertible A
inst✝² : Invertible C
inst✝¹ : Invertible (⅟C + V * ⅟A * U)
inst✝ : Invertible (A + U * C * V)
this : Invertible (A + U * C * V) := A.invertibleAddMulMul U C V
⊢ ⅟(A + U * C * V) = ⅟A - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * V * ⅟A
-- Mathlib/Combinatorics/Colex.lean
/-- `{a} ≤ s` in colex iff `s` contains an element greater than or equal to `a`. -/
lemma singleton_le_toColex : (toColex {a} : Colex α) ≤ toColex s ↔ ∃ x ∈ s, a ≤ x

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x

Tactic:
by_cases a ∈ s <;> aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ { ofColex := {a} } ≤ { ofColex := s } ↔ ∃ x ∈ s, a ≤ x

Tactic:
simp [toColex_le_toColex]

Result:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (a ∉ s → ∃ b ∈ s, ¬b = a ∧ a ≤ b) ↔ ∃ x ∈ s, a ≤ x
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem image_eq (s : Set H) : I '' s = I.symm ⁻¹' s ∩ range I

Proof state:
case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ I.target ∩ ↑I.symm ⁻¹' s = ↑I.symm ⁻¹' s ∩ range ↑I

Tactic:
rw [inter_comm, I.target_eq, I.toPartialEquiv_coe_symm]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ ↑I '' s = ↑I.symm ⁻¹' s ∩ range ↑I

Tactic:
refine (I.toPartialEquiv.image_eq_target_inter_inv_preimage ?_).trans ?_

Result:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ I.source

case refine_2
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ I.target ∩ ↑I.symm ⁻¹' s = ↑I.symm ⁻¹' s ∩ range ↑I

Proof state:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ I.source

Tactic:
rw [I.source_eq]

Result:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ univ

Proof state:
case refine_1
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_3
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
s : Set H
⊢ s ⊆ univ

Tactic:
exact subset_univ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueD_eraseKey_self {β : Type v} [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)}
    {k : α} {fallback : β} (hl : DistinctKeys l) :
    getValueD k (eraseKey k l) fallback = fallback

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k : α
fallback : β
hl : DistinctKeys l
⊢ getValueD k (eraseKey k l) fallback = fallback

Tactic:
simp [getValueD_eq_getValue?, getValue?_eraseKey_self hl]

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
lemma iIndepSets.ae_isProbabilityMeasure (h : iIndepSets π κ μ) :
    ∀ᵐ a ∂μ, IsProbabilityMeasure (κ a)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
⊢ ∀ᵐ (a : α) ∂μ, IsProbabilityMeasure (κ a)

Tactic:
filter_upwards [h.meas_biInter ∅ (f := fun _ ↦ Set.univ) (by simp)] with a ha

Result:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ IsProbabilityMeasure (κ a)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ (κ a) univ = 1

Tactic:
simpa using ha

Result:
no goals

Proof state:
case h
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
a : α
ha : (κ a) (⋂ i ∈ ∅, univ) = ∏ i ∈ ∅, (κ a) univ
⊢ IsProbabilityMeasure (κ a)

Tactic:
exact ⟨by simpa using ha⟩

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
π : ι → Set (Set Ω)
h : iIndepSets π κ μ
⊢ ∀ i ∈ ∅, (fun x => univ) i ∈ π i

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem injective_zpow_iff_not_isOfFinOrder : (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x

Proof state:
G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x

Tactic:
refine ⟨?_, fun h n m hnm => ?_⟩

Result:
case refine_1
G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n => x ^ n) → ¬IsOfFinOrder x

case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m

Proof state:
G : Type u_1
inst✝ : Group G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ (fun n => x ^ n) ↑n = (fun n => x ^ n) 0

Tactic:
simpa using hx

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
x : G
h : ¬IsOfFinOrder x
n m : ℤ
hnm : (fun n => x ^ n) n = (fun n => x ^ n) m
⊢ n = m

Tactic:
rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm

Result:
no goals

Proof state:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False

Tactic:
exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n => x ^ n) → ¬IsOfFinOrder x

Tactic:
simp_rw [isOfFinOrder_iff_pow_eq_one]

Result:
case refine_1
G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n => x ^ n) → ¬∃ n, 0 < n ∧ x ^ n = 1

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
x : G
⊢ (Injective fun n => x ^ n) → ¬∃ n, 0 < n ∧ x ^ n = 1

Tactic:
rintro h ⟨n, hn, hx⟩

Result:
case refine_1.intro.intro
G : Type u_1
inst✝ : Group G
x : G
h : Injective fun n => x ^ n
n : ℕ
hn : 0 < n
hx : x ^ n = 1
⊢ False
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translationNumber_eq_int_iff (hf : Continuous f) {m : ℤ} :
    τ f = m ↔ ∃ x : ℝ, f x = x + m

Proof state:
case mpr.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
x : ℝ
hx : f x = x + ↑m
⊢ τ f = ↑m

Tactic:
exact f.translationNumber_of_eq_add_int hx

Result:
no goals

Proof state:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ τ f = ↑m → ∃ x, f x = x + ↑m

Tactic:
intro h

Result:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + ↑m

Proof state:
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ τ f = ↑m ↔ ∃ x, f x = x + ↑m

Tactic:
constructor

Result:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ τ f = ↑m → ∃ x, f x = x + ↑m

case mpr
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ (∃ x, f x = x + ↑m) → τ f = ↑m

Proof state:
case mpr
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
⊢ (∃ x, f x = x + ↑m) → τ f = ↑m

Tactic:
rintro ⟨x, hx⟩

Result:
case mpr.intro
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
x : ℝ
hx : f x = x + ↑m
⊢ τ f = ↑m

Proof state:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + τ f

Tactic:
exact f.exists_eq_add_translationNumber hf

Result:
no goals

Proof state:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + ↑m

Tactic:
simp only [← h]

Result:
case mp
f : CircleDeg1Lift
hf : Continuous ⇑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, f x = x + τ f
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem if_true_right  (p : Prop) [h : Decidable p] (t : Bool) :
    (ite p t true) = (!(p : Bool) || t)

Proof state:
p : Prop
h : Decidable p
t : Bool
⊢ (if p then t else true) = (!decide p || t)

Tactic:
cases h with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ : Prop
t : Bool
p : p✝
⊢ (if p✝ then t else true) = (!decide p✝ || t)

Tactic:
simp [p]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_lt_iff_lt_mul : a * b⁻¹ < c ↔ a < c * b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a * b⁻¹ < c ↔ a < c * b

Tactic:
rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right]

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
@[to_additive (attr := simp)] lemma map_mk'_self : N.map (mk' N) = ⊥

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
⊢ Subgroup.map (mk' N) N = ⊥

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem Const.get_eq_getValue [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α]
    {m : Raw₀ α (fun _ => β)} (hm : Raw.WFImp m.1) {a : α} {h} :
    Const.get m a h = getValue a (toListModel m.1.buckets) (contains_eq_containsKey hm ▸ h)

Proof state:
α : Type u
β : Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α fun x => β
hm : Raw.WFImp m.val
a : α
h : m.contains a = true
⊢ get m a h = getValue a (toListModel m.val.buckets) ⋯

Tactic:
rw [Const.get_eq_getₘ, Const.getₘ_eq_getValue hm]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem monomial_mul_monomial (n m : ℕ) (r s : R) :
    monomial n r * monomial m s = monomial (n + m) (r * s) :=
  toFinsupp_injective <| by
    simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]

Proof state:
R : Type u
inst✝ : Semiring R
n m : ℕ
r s : R
⊢ ((monomial n) r * (monomial m) s).toFinsupp = ((monomial (n + m)) (r * s)).toFinsupp

Tactic:
simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]

Result:
no goals
-- Mathlib/Analysis/Complex/IsIntegral.lean
theorem isIntegral_int_I : IsIntegral ℤ I

Proof state:
⊢ eval₂ (algebraMap ℤ ℂ) I (X ^ 2 + C 1) = 0

Tactic:
rw [eval₂_add, eval₂_X_pow, eval₂_C, I_sq, eq_intCast, Int.cast_one, neg_add_cancel]

Result:
no goals

Proof state:
⊢ IsIntegral ℤ I

Tactic:
refine ⟨X ^ 2 + C 1, monic_X_pow_add_C _ two_ne_zero, ?_⟩

Result:
⊢ eval₂ (algebraMap ℤ ℂ) I (X ^ 2 + C 1) = 0
-- Mathlib/Geometry/Euclidean/Basic.lean
theorem orthogonalProjection_mem_subspace_eq_self {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] (p : s) : orthogonalProjection s p = 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 : ↥s
⊢ (orthogonalProjection s) ↑p = p

Tactic:
ext

Result:
case a
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 : ↥s
⊢ ↑((orthogonalProjection s) ↑p) = ↑p

Proof state:
case a
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 : ↥s
⊢ ↑((orthogonalProjection s) ↑p) = ↑p

Tactic:
rw [orthogonalProjection_eq_self_iff]

Result:
case a
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 : ↥s
⊢ ↑p ∈ s

Proof state:
case a
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 : ↥s
⊢ ↑p ∈ s

Tactic:
exact p.2

Result:
no goals