harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem coprime_of_coprime (hc : Int.gcd x y = 1) : Int.gcd y z = 1

Proof state:
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ False

Tactic:
apply hp.not_dvd_one

Result:
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ 1

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ ↑p ∣ z * z - y * y

Tactic:
rw [← Int.natCast_dvd] at hpy hpz

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : ↑p ∣ y
hpz : ↑p ∣ z
⊢ ↑p ∣ z * z - y * y

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ ↑p ∣ x ^ 2

Tactic:
rw [sq, eq_sub_of_add_eq h]

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ ↑p ∣ z * z - y * y

Proof state:
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ 1

Tactic:
rw [← hc]

Result:
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ x.gcd y

Proof state:
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ p ∣ x.gcd y

Tactic:
apply Nat.dvd_gcd (Int.Prime.dvd_natAbs_of_coe_dvd_sq hp _ _) hpy

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ ↑p ∣ x ^ 2

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
⊢ False

Tactic:
obtain ⟨p, hp, hpy, hpz⟩ := Nat.Prime.not_coprime_iff_dvd.mp H

Result:
case intro.intro.intro
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : p ∣ y.natAbs
hpz : p ∣ z.natAbs
⊢ False

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
p : ℕ
hp : Nat.Prime p
hpy : ↑p ∣ y
hpz : ↑p ∣ z
⊢ ↑p ∣ z * z - y * y

Tactic:
exact dvd_sub (hpz.mul_right _) (hpy.mul_right _)

Result:
no goals

Proof state:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ y.gcd z = 1

Tactic:
by_contra H

Result:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
H : ¬y.gcd z = 1
⊢ False
-- Mathlib/Data/ENNReal/Inv.lean
lemma mul_iSup (a : ℝ≥0∞) (f : ι → ℝ≥0∞) : a * ⨆ i, f i = ⨆ i, a * f i

Proof state:
case neg.inr.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
exact (mulLeftOrderIso _ <| isUnit_iff.2 ⟨ha₀, ha⟩).map_iSup _

Result:
no goals

Proof state:
case neg
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
obtain rfl | ha₀ := eq_or_ne a 0

Result:
case neg.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ 0 * ⨆ i, f i = ⨆ i, 0 * f i

case neg.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Proof state:
case pos
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
simp [hf]

Result:
no goals

Proof state:
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
by_cases hf : ∀ i, f i = 0

Result:
case pos
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

case neg
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Proof state:
case neg.inr.inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ⊤ ≠ 0
i : ι
hi : ¬f i = 0
⊢ ⊤ * ⨆ i, f i = ⨆ i, ⊤ * f i

Tactic:
simpa [iSup_eq_zero.not.2 hf, eq_comm (a := ⊤)]
  using le_iSup_of_le (f := fun i => ⊤ * f i) i (top_mul hi).ge

Result:
no goals

Proof state:
case neg.inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ⊤ ≠ 0
⊢ ⊤ * ⨆ i, f i = ⨆ i, ⊤ * f i

Tactic:
obtain ⟨i, hi⟩ := not_forall.1 hf

Result:
case neg.inr.inl.intro
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ⊤ ≠ 0
i : ι
hi : ¬f i = 0
⊢ ⊤ * ⨆ i, f i = ⨆ i, ⊤ * f i

Proof state:
case neg.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Tactic:
obtain rfl | ha := eq_or_ne a ∞

Result:
case neg.inr.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : ⊤ ≠ 0
⊢ ⊤ * ⨆ i, f i = ⨆ i, ⊤ * f i

case neg.inr.inr
ι : Sort u_1
a : ℝ≥0∞
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
ha₀ : a ≠ 0
ha : a ≠ ⊤
⊢ a * ⨆ i, f i = ⨆ i, a * f i

Proof state:
case neg.inl
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ¬∀ (i : ι), f i = 0
⊢ 0 * ⨆ i, f i = ⨆ i, 0 * f i

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma monotone_rpow_of_base_ge_one {b : ℝ} (hb : 1 ≤ b) :
    Monotone (b ^ · : ℝ → ℝ)

Proof state:
case inl
b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone fun x => b ^ x

case inr
hb : 1 ≤ 1
⊢ Monotone fun x => 1 ^ x

Tactic:
case inl => exact (strictMono_rpow_of_base_gt_one hb).monotone

Result:
case inr
hb : 1 ≤ 1
⊢ Monotone fun x => 1 ^ x

Proof state:
b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone fun x => b ^ x

Tactic:
exact (strictMono_rpow_of_base_gt_one hb).monotone

Result:
no goals

Proof state:
hb : 1 ≤ 1
⊢ Monotone fun x => 1 ^ x

Tactic:
intro _ _ _

Result:
hb : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x => 1 ^ x) a✝¹ ≤ (fun x => 1 ^ x) b✝

Proof state:
case inr
hb : 1 ≤ 1
⊢ Monotone fun x => 1 ^ x

Tactic:
case inr => intro _ _ _; simp

Result:
no goals

Proof state:
b : ℝ
hb : 1 ≤ b
⊢ Monotone fun x => b ^ x

Tactic:
rcases lt_or_eq_of_le hb with hb | rfl

Result:
case inl
b : ℝ
hb✝ : 1 ≤ b
hb : 1 < b
⊢ Monotone fun x => b ^ x

case inr
hb : 1 ≤ 1
⊢ Monotone fun x => 1 ^ x

Proof state:
hb : 1 ≤ 1
a✝¹ b✝ : ℝ
a✝ : a✝¹ ≤ b✝
⊢ (fun x => 1 ^ x) a✝¹ ≤ (fun x => 1 ^ x) b✝

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem DifferentiableWithinAt.of_dslope (h : DifferentiableWithinAt 𝕜 (dslope f a) s b) :
    DifferentiableWithinAt 𝕜 f s b

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : DifferentiableWithinAt 𝕜 (dslope f a) s b
⊢ DifferentiableWithinAt 𝕜 f s b

Tactic:
simpa only [id, sub_smul_dslope f a, sub_add_cancel] using
  ((differentiableWithinAt_id.sub_const a).smul h).add_const (f a)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Basic.lean
theorem IsDAG.empty {α : Type} : IsDAG α #[]

Proof state:
α : Type
i lhs rhs : Nat
linv rinv : Bool
h : i < #[].size
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i

Tactic:
simp only [Array.size_toArray, List.length_nil] at h

Result:
α : Type
i lhs rhs : Nat
linv rinv : Bool
h✝ : i < #[].size
h : i < 0
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i

Proof state:
α : Type
⊢ IsDAG α #[]

Tactic:
intro i lhs rhs linv rinv h

Result:
α : Type
i lhs rhs : Nat
linv rinv : Bool
h : i < #[].size
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i

Proof state:
α : Type
i lhs rhs : Nat
linv rinv : Bool
h✝ : i < #[].size
h : i < 0
⊢ #[][i] = Decl.gate lhs rhs linv rinv → lhs < i ∧ rhs < i

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem edist_congr_left {x y z : α} (h : edist x y = 0) : edist z x = edist z y

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z

Tactic:
apply edist_congr_right h

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist z x = edist z y

Tactic:
rw [edist_comm z x, edist_comm z y]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y z : α
h : edist x y = 0
⊢ edist x z = edist y z
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.symm {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    {s₁ s₂ : Set (Set Ω)} (h : IndepSets s₁ s₂ κ μ) :
    IndepSets s₂ s₁ κ μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
⊢ IndepSets s₂ s₁ κ μ

Tactic:
intros t1 t2 ht1 ht2

Result:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
filter_upwards [h t2 t1 ht2 ht1] with a ha

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
ha : (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1
⊢ (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
s₁ s₂ : Set (Set Ω)
h : IndepSets s₁ s₂ κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₂
ht2 : t2 ∈ s₁
a : α
ha : (κ a) (t2 ∩ t1) = (κ a) t2 * (κ a) t1
⊢ (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
rwa [Set.inter_comm, mul_comm]

Result:
no goals
-- Mathlib/Data/Finsupp/Defs.lean
theorem mapRange_add [AddZeroClass N] {f : M → N} {hf : f 0 = 0}
    (hf' : ∀ x y, f (x + y) = f x + f y) (v₁ v₂ : α →₀ M) :
    mapRange f hf (v₁ + v₂) = mapRange f hf v₁ + mapRange f hf v₂ :=
  ext fun _ => by simp only [hf', add_apply, mapRange_apply]

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : AddZeroClass M
inst✝ : AddZeroClass N
f : M → N
hf : f 0 = 0
hf' : ∀ (x y : M), f (x + y) = f x + f y
v₁ v₂ : α →₀ M
x✝ : α
⊢ (mapRange f hf (v₁ + v₂)) x✝ = (mapRange f hf v₁ + mapRange f hf v₂) x✝

Tactic:
simp only [hf', add_apply, mapRange_apply]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/Support.lean
theorem mulSupport_comp_inv_smul₀ [One γ] {c : α} (hc : c ≠ 0) (f : β → γ) :
    (mulSupport fun x ↦ f (c⁻¹ • x)) = c • mulSupport f

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f

Tactic:
simp only [mem_smul_set_iff_inv_smul_mem₀ hc, mem_mulSupport]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
hc : c ≠ 0
f : β → γ
⊢ (mulSupport fun x => f (c⁻¹ • x)) = c • mulSupport f

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : GroupWithZero α
inst✝¹ : MulAction α β
inst✝ : One γ
c : α
hc : c ≠ 0
f : β → γ
x : β
⊢ (x ∈ mulSupport fun x => f (c⁻¹ • x)) ↔ x ∈ c • mulSupport f
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.comp {ι' : Type*} {v : ι → E} (hv : Orthonormal 𝕜 v) (f : ι' → ι)
    (hf : Function.Injective f) : Orthonormal 𝕜 (v ∘ f)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
⊢ ∀ (i j : ι'), inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0

Tactic:
intro i j

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
⊢ inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
⊢ Orthonormal 𝕜 (v ∘ f)

Tactic:
classical
rw [orthonormal_iff_ite] at hv ⊢
intro i j
convert hv (f i) (f j) using 1
simp [hf.eq_iff]

Result:
no goals

Proof state:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
⊢ (if i = j then 1 else 0) = if f i = f j then 1 else 0

Tactic:
simp [hf.eq_iff]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
⊢ inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0

Tactic:
convert hv (f i) (f j) using 1

Result:
case h.e'_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
i j : ι'
⊢ (if i = j then 1 else 0) = if f i = f j then 1 else 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : Orthonormal 𝕜 v
f : ι' → ι
hf : Function.Injective f
⊢ Orthonormal 𝕜 (v ∘ f)

Tactic:
rw [orthonormal_iff_ite] at hv ⊢

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
ι' : Type u_5
v : ι → E
hv : ∀ (i j : ι), inner (v i) (v j) = if i = j then 1 else 0
f : ι' → ι
hf : Function.Injective f
⊢ ∀ (i j : ι'), inner ((v ∘ f) i) ((v ∘ f) j) = if i = j then 1 else 0
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_cos_sq_sub_sin_sq :
    ∫ x in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a

Tactic:
simpa only [sq, sub_eq_add_neg, neg_mul_eq_mul_neg] using
  integral_deriv_mul_eq_sub (fun x _ => hasDerivAt_sin x) (fun x _ => hasDerivAt_cos x)
    continuousOn_cos.intervalIntegrable continuousOn_sin.neg.intervalIntegrable

Result:
no goals
-- Mathlib/SetTheory/Cardinal/ToNat.lean
@[simp]
lemma toNat_eq_zero : toNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c

Proof state:
c : Cardinal.{u}
⊢ toNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c

Tactic:
rw [← toNat_toENat, ENat.toNat_eq_zero, toENat_eq_zero, toENat_eq_top]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- Along a mono that is not an iso, the cardinality of the fiber strictly increases. -/
lemma lt_card_fiber_of_mono_of_notIso {X Y : C} (f : X ⟶ Y) [Mono f]
    (h : ¬ IsIso f) : Nat.card (F.obj X) < Nat.card (F.obj Y)

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : Nat.card (F.obj Y).carrier ≤ Nat.card (F.obj X).carrier
⊢ Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier

Tactic:
exact Nat.le_antisymm
  (Finite.card_le_of_injective (F.map f) (injective_of_mono_of_preservesPullback (F.map f))) hlt

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
⊢ Nat.card (F.obj X).carrier < Nat.card (F.obj Y).carrier

Tactic:
by_contra hlt

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).carrier < Nat.card (F.obj Y).carrier
⊢ False

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).carrier < Nat.card (F.obj Y).carrier
⊢ False

Tactic:
apply h

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).carrier < Nat.card (F.obj Y).carrier
⊢ IsIso f

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).carrier < Nat.card (F.obj Y).carrier
⊢ Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier

Tactic:
simp only [gt_iff_lt, not_lt] at hlt

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : Nat.card (F.obj Y).carrier ≤ Nat.card (F.obj X).carrier
⊢ Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).carrier < Nat.card (F.obj Y).carrier
⊢ IsIso f

Tactic:
apply isIso_of_mono_of_eq_card_fiber F f

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
inst✝² : PreGaloisCategory C
inst✝¹ : FiberFunctor F
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ¬IsIso f
hlt : ¬Nat.card (F.obj X).carrier < Nat.card (F.obj Y).carrier
⊢ Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier
-- Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
theorem exists_finsupp_right (x : M ⊗[R] N) :
    ∃ S : N →₀ M, x = S.sum fun n m ↦ m ⊗ₜ[R] n

Proof state:
case intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n => m ⊗ₜ[R] n
⊢ (TensorProduct.comm R M N) x = (TensorProduct.comm R M N) (S.sum fun n m => m ⊗ₜ[R] n)

Tactic:
simp_rw [h, Finsupp.sum, map_sum, comm_tmul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
⊢ ∃ S, x = S.sum fun n m => m ⊗ₜ[R] n

Tactic:
obtain ⟨S, h⟩ := exists_finsupp_left (TensorProduct.comm R M N x)

Result:
case intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x = S.sum fun n m => m ⊗ₜ[R] n

Proof state:
case intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n => m ⊗ₜ[R] n
⊢ ∃ S, x = S.sum fun n m => m ⊗ₜ[R] n

Tactic:
refine ⟨S, (TensorProduct.comm R M N).injective ?_⟩

Result:
case intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M ⊗[R] N
S : N →₀ M
h : (TensorProduct.comm R M N) x = S.sum fun m n => m ⊗ₜ[R] n
⊢ (TensorProduct.comm R M N) x = (TensorProduct.comm R M N) (S.sum fun n m => m ⊗ₜ[R] n)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_filterMap_of_inv (f : α → Option β) (g : β → α) (H : ∀ x : α, (f x).map g = some x)
    (l : Array α) : map g (filterMap f l) = l

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
g : β → α
H : ∀ (x : α), Option.map g (f x) = some x
l : Array α
⊢ map g (filterMap f l) = l

Tactic:
simp only [map_filterMap, H, filterMap_some, id]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/ErdosKaplansky.lean
theorem lift_rank_lt_rank_dual' {V : Type v} [AddCommGroup V] [Module K V]
    (h : ℵ₀ ≤ Module.rank K V) :
    Cardinal.lift.{u} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Proof state:
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
obtain ⟨⟨ι, b⟩⟩ := Module.Free.exists_basis (R := K) (M := V)

Result:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Proof state:
case intro.mk.hb
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ Nontrivial K

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ lift.{u, v} (Module.rank K V) < Module.rank Kᵐᵒᵖ (V →ₗ[K] K)

Tactic:
rw [← b.mk_eq_rank'', rank_dual_eq_card_dual_of_aleph0_le_rank' h,
    ← (b.constr ℕ (M' := K)).toEquiv.cardinal_eq, mk_arrow]

Result:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι

Proof state:
case intro.mk.hb
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ 1 < lift.{v, u} #K

Tactic:
erw [nat_lt_lift_iff, one_lt_iff_nontrivial]

Result:
case intro.mk.hb
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ Nontrivial K

Proof state:
case intro.mk
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ lift.{u, v} #ι < lift.{v, u} #K ^ lift.{u, v} #ι

Tactic:
apply cantor'

Result:
case intro.mk.hb
K : Type u
inst✝² : DivisionRing K
V : Type v
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
ι : Type v
b : Basis ι K V
⊢ 1 < lift.{v, u} #K