harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem finrank_eq_one_iff [Module.Free K V] (ι : Type*) [Unique ι] :
    finrank K V = 1 ↔ Nonempty (Basis ι K V)

Proof state:
case mp
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ finrank K V = 1 → Nonempty (Basis ι K V)

Tactic:
intro h

Result:
case mp
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
⊢ Nonempty (Basis ι K V)

Proof state:
case mpr
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ Nonempty (Basis ι K V) → finrank K V = 1

Tactic:
rintro ⟨b⟩

Result:
case mpr.intro
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
b : Basis ι K V
⊢ finrank K V = 1

Proof state:
case mpr.intro
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
b : Basis ι K V
⊢ finrank K V = 1

Tactic:
simpa using finrank_eq_card_basis b

Result:
no goals

Proof state:
case mp
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
⊢ Nonempty (Basis ι K V)

Tactic:
exact ⟨Module.basisUnique ι h⟩

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ finrank K V = 1 ↔ Nonempty (Basis ι K V)

Tactic:
constructor

Result:
case mp
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ finrank K V = 1 → Nonempty (Basis ι K V)

case mpr
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
ι : Type u_1
inst✝ : Unique ι
⊢ Nonempty (Basis ι K V) → finrank K V = 1
-- Mathlib/Topology/MetricSpace/Antilipschitz.lean
theorem injective {α : Type*} {β : Type*} [EMetricSpace α] [PseudoEMetricSpace β]
    {K : ℝ≥0} {f : α → β} (hf : AntilipschitzWith K f) : Function.Injective f := fun x y h => by
  simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y

Proof state:
α : Type u_4
β : Type u_5
inst✝¹ : EMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
h : f x = f y
⊢ x = y

Tactic:
simpa only [h, edist_self, mul_zero, edist_le_zero] using hf x y

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem csInf_Ioi [NoMaxOrder α] [DenselyOrdered α] : sInf (Ioi a) = a :=
  csInf_eq_of_forall_ge_of_forall_gt_exists_lt nonempty_Ioi (fun _ => le_of_lt) fun w hw => by
    simpa using exists_between hw

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLattice α
a : α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
w : α
hw : a < w
⊢ ∃ a_1 ∈ Ioi a, a_1 < w

Tactic:
simpa using exists_between hw

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem contDiffWithinAt_infty :
    ContDiffWithinAt 𝕜 ∞ f s x ↔ ∀ n : ℕ, ContDiffWithinAt 𝕜 n f s x :=
  contDiffWithinAt_iff_forall_nat_le.trans <| by simp only [forall_prop_of_true, le_top]

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
⊢ (∀ (m : ℕ), ↑m ≤ ⊤ → ContDiffWithinAt 𝕜 (↑m) f s x) ↔ ∀ (n : ℕ), ContDiffWithinAt 𝕜 (↑n) f s x

Tactic:
simp only [forall_prop_of_true, le_top]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem liftOrGet_none_left {f} {b : Option α} : liftOrGet f none b = b

Proof state:
α : Type u_1
f : α → α → α
b : Option α
⊢ liftOrGet f none b = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_add' (hx : 0 ≤ x) (h : y + z ≠ 0) : x ^ (y + z) = x ^ y * x ^ z

Proof state:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0

Tactic:
have : y ≠ 0 ∨ z ≠ 0 := not_and_or.1 fun ⟨hy, hz⟩ => h <| hy.symm ▸ hz.symm ▸ zero_add 0

Result:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
this : y ≠ 0 ∨ z ≠ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0

Proof state:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

Tactic:
rw [zero_rpow h, zero_eq_mul]

Result:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0

Proof state:
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
rcases hx.eq_or_lt with (rfl | pos)

Result:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
⊢ 0 ^ (y + z) = 0 ^ y * 0 ^ z

case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Proof state:
case inr
x y z : ℝ
hx : 0 ≤ x
h : y + z ≠ 0
pos : 0 < x
⊢ x ^ (y + z) = x ^ y * x ^ z

Tactic:
exact rpow_add pos _ _

Result:
no goals

Proof state:
case inl
y z : ℝ
h : y + z ≠ 0
hx : 0 ≤ 0
this : y ≠ 0 ∨ z ≠ 0
⊢ 0 ^ y = 0 ∨ 0 ^ z = 0

Tactic:
exact this.imp zero_rpow zero_rpow

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Lemmas.lean
theorem inter_empty (s : Finset α) : s ∩ ∅ = ∅ :=
  ext fun _ => mem_inter.trans <| by simp

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ : α
⊢ x✝ ∈ s ∧ x✝ ∈ ∅ ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_eq_none [BEq α] {l : List ((a : α) × β a)} {a : α} :
    getEntry? a l = none ↔ containsKey a l = false

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
⊢ getEntry? a l = none ↔ containsKey a l = false

Tactic:
rw [← Option.not_isSome_iff_eq_none, Bool.not_eq_true, ← containsKey_eq_isSome_getEntry?]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem abs_real_inner_div_norm_mul_norm_le_one (x y : F) : |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ 0 ≤ ‖x‖ * ‖y‖

Tactic:
positivity

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ |⟪x, y⟫_ℝ| / (‖x‖ * ‖y‖) ≤ 1

Tactic:
exact div_le_one_of_le₀ (abs_real_inner_le_norm x y) (by positivity)

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ |⟪x, y⟫_ℝ / (‖x‖ * ‖y‖)| ≤ 1

Tactic:
rw [abs_div, abs_mul, abs_norm, abs_norm]

Result:
F : Type u_3
inst✝¹ : SeminormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
⊢ |⟪x, y⟫_ℝ| / (‖x‖ * ‖y‖) ≤ 1
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem normal_mul (N H : Subgroup G) [N.Normal] : (↑(N ⊔ H) : Set G) = N * H

Proof state:
G : Type u_2
inst✝¹ : Group G
N H : Subgroup G
inst✝ : N.Normal
⊢ ↑(N ⊔ H) = ↑N * ↑H

Tactic:
rw [← set_mul_normal_comm, sup_comm, mul_normal]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Ordinal.lean
theorem IsTransitive.union (hx : x.IsTransitive) (hy : y.IsTransitive) :
    (x ∪ y).IsTransitive

Proof state:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ (x ∪ y).IsTransitive

Tactic:
rw [← sUnion_pair]

Result:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ (⋃₀ {x, y}).IsTransitive

Proof state:
case H.inl
y : ZFSet.{u}
hy : y.IsTransitive
y✝ : ZFSet.{u}
hx : y✝.IsTransitive
⊢ y✝.IsTransitive

case H.inr
x : ZFSet.{u}
hx : x.IsTransitive
y✝ : ZFSet.{u}
hy : y✝.IsTransitive
⊢ y✝.IsTransitive

Tactic:
assumption'

Result:
no goals

Proof state:
case H
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ ∀ y_1 ∈ {x, y}, y_1.IsTransitive

Tactic:
intro

Result:
case H
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ ∈ {x, y} → y✝.IsTransitive

Proof state:
case H
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ ∈ {x, y} → y✝.IsTransitive

Tactic:
rw [mem_pair]

Result:
case H
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ = x ∨ y✝ = y → y✝.IsTransitive

Proof state:
case H
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ = x ∨ y✝ = y → y✝.IsTransitive

Tactic:
rintro (rfl | rfl)

Result:
case H.inl
y : ZFSet.{u}
hy : y.IsTransitive
y✝ : ZFSet.{u}
hx : y✝.IsTransitive
⊢ y✝.IsTransitive

case H.inr
x : ZFSet.{u}
hx : x.IsTransitive
y✝ : ZFSet.{u}
hy : y✝.IsTransitive
⊢ y✝.IsTransitive

Proof state:
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ (⋃₀ {x, y}).IsTransitive

Tactic:
apply IsTransitive.sUnion'

Result:
case H
x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
⊢ ∀ y_1 ∈ {x, y}, y_1.IsTransitive
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
/-- If `p` is a finite formal multilinear series, then so is `p.changeOriginSeries k` for every
`k` in `ℕ`. More precisely, if `p m = 0` for `n ≤ m`, then `p.changeOriginSeries k m = 0` for
`n ≤ k + m`. -/
lemma changeOriginSeries_finite_of_finite (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ}
    (hn : ∀ (m : ℕ), n ≤ m → p m = 0) (k : ℕ) : ∀ {m : ℕ}, n ≤ k + m →
    p.changeOriginSeries k m = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ ∑ s : { s // s.card = m }, p.changeOriginSeriesTerm k m ↑s ⋯ = 0

Tactic:
exact Finset.sum_eq_zero (fun _ _ => p.changeOriginSeriesTerm_bound hn _ _ _ hm)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ p.changeOriginSeries k m = 0

Tactic:
rw [changeOriginSeries]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ ∑ s : { s // s.card = m }, p.changeOriginSeriesTerm k m ↑s ⋯ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
⊢ ∀ {m : ℕ}, n ≤ k + m → p.changeOriginSeries k m = 0

Tactic:
intro m hm

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ p.changeOriginSeries k m = 0
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma prodMkRight_zero : Kernel.prodMkRight α (0 : Kernel β γ) = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
⊢ prodMkRight α 0 = 0

Tactic:
ext x s _

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : β × α
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkRight α 0) x) s = (0 x) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
x : β × α
s : Set γ
a✝ : MeasurableSet s
⊢ ((prodMkRight α 0) x) s = (0 x) s

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Surreal/Basic.lean
theorem moveRight {x : PGame} (o : Numeric x) (j : x.RightMoves) : Numeric (x.moveRight j)

Proof state:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
j : (PGame.mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ ((PGame.mk α✝ β✝ a✝¹ a✝).moveRight j).Numeric

Tactic:
exact o.2.2 j

Result:
no goals

Proof state:
x : PGame
o : x.Numeric
j : x.RightMoves
⊢ (x.moveRight j).Numeric

Tactic:
cases x

Result:
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
o : (PGame.mk α✝ β✝ a✝¹ a✝).Numeric
j : (PGame.mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ ((PGame.mk α✝ β✝ a✝¹ a✝).moveRight j).Numeric
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem mem_source : x ∈ e.source ↔ proj x ∈ e.baseSet

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
x : Z
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet

Tactic:
rw [e.source_eq, mem_preimage]

Result:
no goals
-- Mathlib/Algebra/Colimit/Module.lean
lemma congr_symm_apply_of (e : (i : ι) → G i ≃+ G' i)
    (he : ∀ i j h, (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp (e i))
    {i : ι} (g : G' i) :
    (congr e he).symm (of G' f' i g) = of G f i ((e i).symm g)

Proof state:
ι : Type u_2
inst✝³ : Preorder ι
G : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (G i)
f : (i j : ι) → i ≤ j → G i →+ G j
inst✝¹ : DecidableEq ι
G' : ι → Type u_5
inst✝ : (i : ι) → AddCommMonoid (G' i)
f' : (i j : ι) → i ≤ j → G' i →+ G' j
e : (i : ι) → G i ≃+ G' i
he : ∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)
i : ι
g : G' i
⊢ (congr e he).symm ((of G' f' i) g) = (of G f i) ((e i).symm g)

Tactic:
simp only [congr, AddMonoidHom.toAddEquiv_symm_apply, map_apply_of, AddMonoidHom.coe_coe]

Result:
no goals
-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean
theorem wittStructureInt_prop (Φ : MvPolynomial idx ℤ) (n) :
    bind₁ (wittStructureInt p Φ) (wittPolynomial p ℤ n) =
      bind₁ (fun i => rename (Prod.mk i) (W_ ℤ n)) Φ

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
this :
  (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
⊢ (map (Int.castRingHom ℚ)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ)

Tactic:
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial,
  AlgHom.coe_toRingHom, map_wittStructureInt]

Result:
no goals

Proof state:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ)

Tactic:
have := wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
this :
  (bind₁ (wittStructureRat p ((map (Int.castRingHom ℚ)) Φ))) (W_ ℚ n) =
    (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ n)) ((map (Int.castRingHom ℚ)) Φ)
⊢ (map (Int.castRingHom ℚ)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ)

Proof state:
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (bind₁ (wittStructureInt p Φ)) (W_ ℤ n) = (bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ

Tactic:
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective

Result:
case a
p : ℕ
idx : Type u_2
hp : Fact (Nat.Prime p)
Φ : MvPolynomial idx ℤ
n : ℕ
⊢ (map (Int.castRingHom ℚ)) ((bind₁ (wittStructureInt p Φ)) (W_ ℤ n)) =
    (map (Int.castRingHom ℚ)) ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℤ n)) Φ)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_mono_ae {f g : α → ℝ} (hf : Integrable f μ) (hg : Integrable g μ) (h : f ≤ᵐ[μ] g) :
    ∫ a, f a ∂μ ≤ ∫ a, g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Tactic:
have A : CompleteSpace ℝ := by infer_instance

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
A : CompleteSpace ℝ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
A : CompleteSpace ℝ
⊢ ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ

Tactic:
simp only [integral, A, L1.integral]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
A : CompleteSpace ℝ
⊢ (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0) ≤
    if h : True then if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
    else 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
A : CompleteSpace ℝ
⊢ (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0) ≤
    if h : True then if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
    else 0

Tactic:
exact setToFun_mono (dominatedFinMeasAdditive_weightedSMul μ)
  (fun s _ _ => weightedSMul_nonneg s) hf hg h

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
h : f ≤ᶠ[ae μ] g
⊢ CompleteSpace ℝ

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem prod_Ico_eq_prod_range (f : ℕ → M) (m n : ℕ) :
    ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Proof state:
case neg
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
rw [Ico_eq_empty_of_le h, tsub_eq_zero_iff_le.mpr h, range_zero, prod_empty, prod_empty]

Result:
no goals

Proof state:
case pos
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
rw [← Nat.Ico_zero_eq_range, prod_Ico_add, zero_add, tsub_add_cancel_of_le h]

Result:
no goals

Proof state:
case neg
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : ¬m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
replace h : n ≤ m := le_of_not_ge h

Result:
case neg
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : n ≤ m
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Proof state:
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

Tactic:
by_cases h : m ≤ n

Result:
case pos
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)

case neg
M : Type u_2
inst✝ : CommMonoid M
f : ℕ → M
m n : ℕ
h : ¬m ≤ n
⊢ ∏ k ∈ Ico m n, f k = ∏ k ∈ range (n - m), f (m + k)
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma norm_jacobiTheta₂_term (n : ℤ) (z τ : ℂ) :
    ‖jacobiTheta₂_term n z τ‖ = rexp (-π * n ^ 2 * τ.im - 2 * π * n * z.im)

Proof state:
n : ℤ
z τ : ℂ
⊢ ‖jacobiTheta₂_term n z τ‖ = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)

Tactic:
rw [jacobiTheta₂_term, Complex.norm_exp, (by push_cast; ring :
  (2 * π : ℂ) * I * n * z + π * I * n ^ 2 * τ = (π * (2 * n):) * z * I + (π * n ^ 2 :) * τ * I),
  add_re, mul_I_re, im_ofReal_mul, mul_I_re, im_ofReal_mul]

Result:
n : ℤ
z τ : ℂ
⊢ rexp (-(π * (2 * ↑n) * z.im) + -(π * ↑n ^ 2 * τ.im)) = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)

Proof state:
n : ℤ
z τ : ℂ
⊢ 2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ = ↑(π * (2 * ↑n)) * z * I + ↑(π * ↑n ^ 2) * τ * I

Tactic:
push_cast

Result:
n : ℤ
z τ : ℂ
⊢ 2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ = ↑π * (2 * ↑n) * z * I + ↑π * ↑n ^ 2 * τ * I

Proof state:
n : ℤ
z τ : ℂ
⊢ rexp (-(π * (2 * ↑n) * z.im) + -(π * ↑n ^ 2 * τ.im)) = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)

Tactic:
ring_nf

Result:
no goals

Proof state:
n : ℤ
z τ : ℂ
⊢ 2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ = ↑π * (2 * ↑n) * z * I + ↑π * ↑n ^ 2 * τ * I

Tactic:
ring

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearMap.linearIndependent_iff (f : M →ₗ[R] M') (hf_inj : LinearMap.ker f = ⊥) :
    LinearIndependent R (f ∘ v) ↔ LinearIndependent R v :=
  f.linearIndependent_iff_of_disjoint <| by simp_rw [hf_inj, disjoint_bot_right]

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M
inst✝ : Module R M'
f : M →ₗ[R] M'
hf_inj : ker f = ⊥
⊢ Disjoint (span R (Set.range v)) (ker f)

Tactic:
simp_rw [hf_inj, disjoint_bot_right]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Presheaf.lean
@[reassoc (attr := simp)]
lemma presheafHom_naturality {P Q : Cᵒᵖ ⥤ Type v₁} (f : P ⟶ Q) :
    presheafHom φ P ≫ whiskerLeft F.op (G.map f) = f ≫ presheafHom φ Q :=
  hom_ext_yoneda (fun X p => yonedaEquiv.injective (by
    rw [← assoc p f, yonedaEquiv_ι_presheafHom, ← assoc,
      yonedaEquiv_comp, yonedaEquiv_ι_presheafHom,
      whiskerLeft_app, Functor.map_comp, FunctorToTypes.comp]
    dsimp))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
P Q : Cᵒᵖ ⥤ Type v₁
f : P ⟶ Q
X : C
p : yoneda.obj X ⟶ P
⊢ yonedaEquiv (p ≫ presheafHom φ P ≫ whiskerLeft F.op (G.map f)) = yonedaEquiv (p ≫ f ≫ presheafHom φ Q)

Tactic:
rw [← assoc p f, yonedaEquiv_ι_presheafHom, ← assoc,
  yonedaEquiv_comp, yonedaEquiv_ι_presheafHom,
  whiskerLeft_app, Functor.map_comp, FunctorToTypes.comp]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
P Q : Cᵒᵖ ⥤ Type v₁
f : P ⟶ Q
X : C
p : yoneda.obj X ⟶ P
⊢ (G.map f).app (F.op.obj (Opposite.op X))
      ((G.map p).app (Opposite.op (F.obj X))
        ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))) =
    (G.map f).app (Opposite.op (F.obj X))
      ((G.map p).app (Opposite.op (F.obj X))
        ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X))))))

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₁, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type v₁) ⥤ Dᵒᵖ ⥤ Type v₁
φ : F ⋙ yoneda ⟶ yoneda ⋙ G
P Q : Cᵒᵖ ⥤ Type v₁
f : P ⟶ Q
X : C
p : yoneda.obj X ⟶ P
⊢ (G.map f).app (F.op.obj (Opposite.op X))
      ((G.map p).app (Opposite.op (F.obj X))
        ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X)))))) =
    (G.map f).app (Opposite.op (F.obj X))
      ((G.map p).app (Opposite.op (F.obj X))
        ((φ.app X).app (Opposite.op (F.obj X)) (𝟙 (Opposite.unop (Opposite.op (F.obj X))))))

Tactic:
dsimp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Rotation.lean
theorem rotation_zero : o.rotation 0 = LinearIsometryEquiv.refl ℝ V

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
⊢ o.rotation 0 = LinearIsometryEquiv.refl ℝ V

Tactic:
ext

Result:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x✝ : V
⊢ (o.rotation 0) x✝ = (LinearIsometryEquiv.refl ℝ V) x✝

Proof state:
case h
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x✝ : V
⊢ (o.rotation 0) x✝ = (LinearIsometryEquiv.refl ℝ V) x✝

Tactic:
simp [rotation]

Result:
no goals