harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_iff_isIso_liftCycles (φ : S₁ ⟶ S₂)
    (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) :
    QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp]))

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Result:
no goals

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
  (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ (KernelFork.ofι S₂.iCycles ⋯) S₂.cyclesIsKernel) :=
  { φK := S₂.liftCycles φ.τ₂ ⋯, φH := S₂.liftCycles φ.τ₂ ⋯, commi := ⋯, commf' := ⋯, commπ := ⋯ }
⊢ QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
exact H.quasiIso_iff

Result:
no goals

Proof state:
C : Type ?u.28359
inst✝⁵ : Category.{?u.28363, ?u.28359} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ φ.τ₂ ≫ S₂.g = 0

Tactic:
rw [φ.comm₂₃, hg₁, zero_comp]

Result:
no goals

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
⊢ QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)

Tactic:
let H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
    (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ _ S₂.cyclesIsKernel) :=
  { φK := S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp])
    φH := S₂.liftCycles φ.τ₂ (by rw [φ.comm₂₃, hg₁, zero_comp]) }

Result:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
H : LeftHomologyMapData φ (LeftHomologyData.ofZeros S₁ hf₁ hg₁)
  (LeftHomologyData.ofIsLimitKernelFork S₂ hf₂ (KernelFork.ofι S₂.iCycles ⋯) S₂.cyclesIsKernel) :=
  { φK := S₂.liftCycles φ.τ₂ ⋯, φH := S₂.liftCycles φ.τ₂ ⋯, commi := ⋯, commf' := ⋯, commπ := ⋯ }
⊢ QuasiIso φ ↔ IsIso (S₂.liftCycles φ.τ₂ ⋯)
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
theorem norm_eq_of_norm_add_lt_left {z1 z2 : ℤ_[p]} (h : ‖z1 + z2‖ < ‖z1‖) : ‖z1‖ = ‖z2‖ :=
  by_contra fun hne =>
    not_lt_of_ge (by rw [norm_add_eq_max_of_ne hne]; apply le_max_left) h

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1 + z2‖ ≥ ‖z1‖

Tactic:
rw [norm_add_eq_max_of_ne hne]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z1‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
z1 z2 : ℤ_[p]
h : ‖z1 + z2‖ < ‖z1‖
hne : ¬‖z1‖ = ‖z2‖
⊢ ‖z1‖ ⊔ ‖z2‖ ≥ ‖z1‖

Tactic:
apply le_max_left

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β → β} :
    (Const.modify m k f).getKey! k = if m.contains k then k else default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
inst✝ : Inhabited α
k : α
f : β → β
⊢ (modify m k f).getKey! k = if m.contains k = true then k else default

Tactic:
simp_to_model [Const.modify] using List.Const.getKey!_modifyKey_self

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma isComplement_iff_existsUnique_mul_inv_mem :
    IsComplement S T ↔ ∀ g, ∃! t : T, g * (t : G)⁻¹ ∈ S

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ (fun t => g * (↑t)⁻¹ ∈ S) x.2

Tactic:
simp [← hx]

Result:
no goals

Proof state:
case h.e'_2.h.a.mpr.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! t, g * (↑t)⁻¹ ∈ S

Tactic:
exact ⟨x.2, by simp [← hx], fun y hy ↦ (Prod.ext_iff.1 <| by simpa using hx' (⟨_, hy⟩, y)).2⟩

Result:
no goals

Proof state:
case h.e'_2.h.a.mp.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑T
hx : g * (↑x)⁻¹ ∈ S
hx' : ∀ (y : ↑T), (fun t => g * (↑t)⁻¹ ∈ S) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
exact ⟨(⟨_, hx⟩, x), by simp, by aesop⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
y : ↑T
hy : (fun t => g * (↑t)⁻¹ ∈ S) y
⊢ ?m.87846 = ?m.87847

Tactic:
simpa using hx' (⟨_, hy⟩, y)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑T
hx : g * (↑x)⁻¹ ∈ S
hx' : ∀ (y : ↑T), (fun t => g * (↑t)⁻¹ ∈ S) y → y = x
⊢ (fun x => ↑x.1 * ↑x.2 = g) (⟨g * (↑x)⁻¹, hx⟩, x)

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
⊢ IsComplement S T ↔ ∀ (g : G), ∃! t, g * (↑t)⁻¹ ∈ S

Tactic:
convert isComplement_iff_existsUnique with g

Result:
case h.e'_2.h.a
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! t, g * (↑t)⁻¹ ∈ S) ↔ ∃! x, ↑x.1 * ↑x.2 = g

Proof state:
case h.e'_2.h.a
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
⊢ (∃! t, g * (↑t)⁻¹ ∈ S) ↔ ∃! x, ↑x.1 * ↑x.2 = g

Tactic:
constructor <;> rintro ⟨x, hx, hx'⟩

Result:
case h.e'_2.h.a.mp.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑T
hx : g * (↑x)⁻¹ ∈ S
hx' : ∀ (y : ↑T), (fun t => g * (↑t)⁻¹ ∈ S) y → y = x
⊢ ∃! x, ↑x.1 * ↑x.2 = g

case h.e'_2.h.a.mpr.intro.intro
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑S × ↑T
hx : ↑x.1 * ↑x.2 = g
hx' : ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = x
⊢ ∃! t, g * (↑t)⁻¹ ∈ S

Proof state:
G : Type u_1
inst✝ : Group G
S T : Set G
g : G
x : ↑T
hx : g * (↑x)⁻¹ ∈ S
hx' : ∀ (y : ↑T), (fun t => g * (↑t)⁻¹ ∈ S) y → y = x
⊢ ∀ (y : ↑S × ↑T), (fun x => ↑x.1 * ↑x.2 = g) y → y = (⟨g * (↑x)⁻¹, hx⟩, x)

Tactic:
aesop

Result:
no goals
-- Mathlib/RingTheory/AdjoinRoot.lean
theorem lift_root : lift i a h (root f) = a

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
f : R[X]
inst✝ : CommRing S
i : R →+* S
a : S
h : eval₂ i a f = 0
⊢ (lift i a h) (root f) = a

Tactic:
rw [root, lift_mk, eval₂_X]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_sign_add_right (x y : V) : (o.oangle x (x + y)).sign = (o.oangle x y).sign

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ (o.oangle x (x + y)).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_smul_add_right x y 1, one_smul]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem orthogonalProjection_circumcenter {n : ℕ} (s : Simplex ℝ P n) {fs : Finset (Fin (n + 1))}
    {m : ℕ} (h : #fs = m + 1) :
    ↑((s.face h).orthogonalProjectionSpan s.circumcenter) = (s.face h).circumcenter :=
  haveI hr : ∃ r, ∀ i, dist ((s.face h).points i) s.circumcenter = r

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = s.circumradius

Tactic:
simp [face_points]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ∃ r, ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = r

Tactic:
use s.circumradius

Result:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = s.circumradius
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem comap_map_mk_uniformity : comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) = 𝓤 α

Tactic:
refine le_antisymm ?_ le_comap_map

Result:
α : Type u
inst✝ : UniformSpace α
⊢ Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α

Proof state:
α : Type u
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x₁ x₂ : α
x✝ : (x₁, x₂) ∈ Prod.map mk mk ⁻¹' (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Prod.map mk mk (y₁, y₂) = Prod.map mk mk (x₁, x₂)
⊢ (x₁, x₂) ∈ id U

Tactic:
simp only [Prod.map, Prod.ext_iff, mk_eq_mk] at hxy

Result:
α : Type u
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x₁ x₂ : α
x✝ : (x₁, x₂) ∈ Prod.map mk mk ⁻¹' (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Inseparable y₁ x₁ ∧ Inseparable y₂ x₂
⊢ (x₁, x₂) ∈ id U

Proof state:
α : Type u
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x₁ x₂ : α
x✝ : (x₁, x₂) ∈ Prod.map mk mk ⁻¹' (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Inseparable y₁ x₁ ∧ Inseparable y₂ x₂
⊢ (x₁, x₂) ∈ id U

Tactic:
exact ((hxy.1.prod hxy.2).mem_open_iff hU.2).1 hyU

Result:
no goals

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)) ≤ 𝓤 α

Tactic:
refine ((((𝓤 α).basis_sets.map _).comap _).le_basis_iff uniformity_hasBasis_open).2 fun U hU ↦ ?_

Result:
α : Type u
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
⊢ ∃ i ∈ 𝓤 α, Prod.map mk mk ⁻¹' (Prod.map mk mk '' id i) ⊆ id U

Proof state:
α : Type u
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
⊢ ∃ i ∈ 𝓤 α, Prod.map mk mk ⁻¹' (Prod.map mk mk '' id i) ⊆ id U

Tactic:
refine ⟨U, hU.1, fun (x₁, x₂) ⟨(y₁, y₂), hyU, hxy⟩ ↦ ?_⟩

Result:
α : Type u
inst✝ : UniformSpace α
U : Set (α × α)
hU : U ∈ 𝓤 α ∧ IsOpen U
x✝¹ : α × α
x₁ x₂ : α
x✝ : (x₁, x₂) ∈ Prod.map mk mk ⁻¹' (Prod.map mk mk '' id U)
y₁ y₂ : α
hyU : (y₁, y₂) ∈ id U
hxy : Prod.map mk mk (y₁, y₂) = Prod.map mk mk (x₁, x₂)
⊢ (x₁, x₂) ∈ id U
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.MeasurableSet.exists_isOpen_diff_lt [OuterRegular μ] {A : Set α}
    (hA : MeasurableSet A) (hA' : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ U, U ⊇ A ∧ IsOpen U ∧ μ U < ∞ ∧ μ (U \ A) < ε

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε

Tactic:
rcases A.exists_isOpen_lt_add hA' hε with ⟨U, hAU, hUo, hU⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : μ U < μ A + ε
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε

Proof state:
case right
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : μ U < μ A + ε
⊢ μ (U \ A) < ε

Tactic:
exact measure_diff_lt_of_lt_add hA.nullMeasurableSet hAU hA' hU

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : μ U < μ A + ε
⊢ ∃ U ⊇ A, IsOpen U ∧ μ U < ⊤ ∧ μ (U \ A) < ε

Tactic:
use U, hAU, hUo, hU.trans_le le_top

Result:
case right
α : Type u_1
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace α
inst✝ : μ.OuterRegular
A : Set α
hA : MeasurableSet A
hA' : μ A ≠ ⊤
ε : ℝ≥0∞
hε : ε ≠ 0
U : Set α
hAU : U ⊇ A
hUo : IsOpen U
hU : μ U < μ A + ε
⊢ μ (U \ A) < ε
-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
@[stacks 01W6 "(1)"]
lemma UniversallyClosed.of_comp_of_isSeparated [UniversallyClosed (f ≫ g)] [IsSeparated g] :
    UniversallyClosed f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : IsSeparated g
this : UniversallyClosed (Limits.pullback.snd (f ≫ g) g)
⊢ UniversallyClosed (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : IsSeparated g
⊢ UniversallyClosed f

Tactic:
rw [← Limits.pullback.lift_snd (𝟙 _) f (Category.id_comp (f ≫ g))]

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : IsSeparated g
⊢ UniversallyClosed (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : IsSeparated g
⊢ UniversallyClosed (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)

Tactic:
have := MorphismProperty.pullback_snd (P := @UniversallyClosed) (f ≫ g) g inferInstance

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : IsSeparated g
this : UniversallyClosed (Limits.pullback.snd (f ≫ g) g)
⊢ UniversallyClosed (Limits.pullback.lift (𝟙 X) f ⋯ ≫ Limits.pullback.snd (f ≫ g) g)
-- Mathlib/Data/Matrix/Mul.lean
theorem vecMul_add [Fintype m] (A B : Matrix m n α) (x : m → α) :
    x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
x✝ : n
⊢ (x ᵥ* (A + B)) x✝ = (x ᵥ* A + x ᵥ* B) x✝

Tactic:
apply dotProduct_add

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
⊢ x ᵥ* (A + B) = x ᵥ* A + x ᵥ* B

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
x : m → α
x✝ : n
⊢ (x ᵥ* (A + B)) x✝ = (x ᵥ* A + x ᵥ* B) x✝
-- Mathlib/Data/Int/Bitwise.lean
theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0

Proof state:
case false
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0

Tactic:
apply (add_zero _).symm

Result:
no goals

Proof state:
b : Bool
n : ℤ
⊢ bit b n = 2 * n + bif b then 1 else 0

Tactic:
cases b

Result:
case false
n : ℤ
⊢ bit false n = 2 * n + bif false then 1 else 0

case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0

Proof state:
case true
n : ℤ
⊢ bit true n = 2 * n + bif true then 1 else 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
lemma IsNontrivial.exists_abv_gt_one {F S : Type*} [Field F] [LinearOrderedField S]
    {v : AbsoluteValue F S} (h : v.IsNontrivial) :
    ∃ x, 1 < v x

Proof state:
case intro.intro.inl
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ ∃ x, 1 < v x

Tactic:
refine ⟨x⁻¹, ?_⟩

Result:
case intro.intro.inl
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ 1 < v x⁻¹

Proof state:
case intro.intro.inl
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ 1 < v x⁻¹

Tactic:
rw [map_inv₀]

Result:
case intro.intro.inl
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ 1 < (v x)⁻¹

Proof state:
case intro.intro.inr
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : 1 < v x
⊢ ∃ x, 1 < v x

Tactic:
exact ⟨x, h⟩

Result:
no goals

Proof state:
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
h : v.IsNontrivial
⊢ ∃ x, 1 < v x

Tactic:
obtain ⟨x, hx₀, hx₁⟩ := h

Result:
case intro.intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
⊢ ∃ x, 1 < v x

Proof state:
case intro.intro
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
⊢ ∃ x, 1 < v x

Tactic:
rcases hx₁.lt_or_lt with h | h

Result:
case intro.intro.inl
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ ∃ x, 1 < v x

case intro.intro.inr
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : 1 < v x
⊢ ∃ x, 1 < v x

Proof state:
case intro.intro.inl
F : Type u_7
S : Type u_8
inst✝¹ : Field F
inst✝ : LinearOrderedField S
v : AbsoluteValue F S
x : F
hx₀ : x ≠ 0
hx₁ : v x ≠ 1
h : v x < 1
⊢ 1 < (v x)⁻¹

Tactic:
exact (one_lt_inv₀ <| v.pos hx₀).mpr h

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem frobenius_verschiebung (x : 𝕎 R) : frobenius (verschiebung x) = x * p

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
⊢ frobenius (verschiebung x) = x * ↑p

Tactic:
have : IsPoly p fun {R} [CommRing R] x ↦ frobenius (verschiebung x) :=
  IsPoly.comp (hg := frobenius_isPoly p) (hf := verschiebung_isPoly)

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this : IsPoly p fun {R} [CommRing R] x => frobenius (verschiebung x)
⊢ frobenius (verschiebung x) = x * ↑p

Proof state:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly p fun {R} [CommRing R] x => frobenius (verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ), (ghostComponent n) (frobenius (verschiebung x)) = (ghostComponent n) (x * ↑p)

Tactic:
ghost_simp [mul_comm]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this✝ : IsPoly p fun {R} [CommRing R] x => frobenius (verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
⊢ frobenius (verschiebung x) = x * ↑p

Tactic:
ghost_calc x

Result:
case refine_3
p : ℕ
hp : Fact (Nat.Prime p)
this✝ : IsPoly p fun {R} [CommRing R] x => frobenius (verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
⊢ ∀ (n : ℕ), (ghostComponent n) (frobenius (verschiebung x)) = (ghostComponent n) (x * ↑p)

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this : IsPoly p fun {R} [CommRing R] x => frobenius (verschiebung x)
⊢ frobenius (verschiebung x) = x * ↑p

Tactic:
have : IsPoly p fun {R} [CommRing R] x ↦ x * p := mulN_isPoly p p

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
this✝ : IsPoly p fun {R} [CommRing R] x => frobenius (verschiebung x)
this : IsPoly p fun {R} [CommRing R] x => x * ↑p
⊢ frobenius (verschiebung x) = x * ↑p
-- Mathlib/Probability/ProbabilityMassFunction/Basic.lean
theorem toPMF_eq_iff_toMeasure_eq (μ : Measure α) [IsProbabilityMeasure μ] :
    μ.toPMF = p ↔ μ = p.toMeasure

Proof state:
α : Type u_1
inst✝³ : Countable α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSingletonClass α
p : PMF α
μ : Measure α
inst✝ : IsProbabilityMeasure μ
⊢ μ.toPMF = p ↔ μ = p.toMeasure

Tactic:
rw [← toMeasure_inj, Measure.toPMF_toMeasure]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
theorem det_fderivPiPolarCoordSymm (p : ι → ℝ × ℝ) :
    (fderivPiPolarCoordSymm p).det = ∏ i, (p i).1

Proof state:
ι : Type u_1
inst✝ : Fintype ι
p : ι → ℝ × ℝ
⊢ (fderivPiPolarCoordSymm p).det = ∏ i : ι, (p i).1

Tactic:
simp_rw [fderivPiPolarCoordSymm, ContinuousLinearMap.det_pi, det_fderivPolarCoordSymm]

Result:
no goals
-- Mathlib/Data/Finset/Filter.lean
lemma _root_.Set.pairwiseDisjoint_filter [DecidableEq β] (f : α → β) (s : Set β) (t : Finset α) :
    s.PairwiseDisjoint fun x ↦ t.filter (f · = x)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) (f x)
⊢ x ∈ t ∧ f x = j

Tactic:
simpa using hj hx

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) (f x)
⊢ x ∈ ⊥

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t u : Finset α
x : α
hx : x ∈ u
hi hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) (f x)
h : f x ≠ f x
⊢ x ∈ ⊥

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
⊢ s.PairwiseDisjoint fun x => filter (fun x_1 => f x_1 = x) t

Tactic:
rintro i - j - h u hi hj x hx

Result:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) i
hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ ⊥

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) i
hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ t ∧ f x = i

Tactic:
simpa using hi hx

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t u : Finset α
x : α
hx : x ∈ u
hi hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) (f x)
h : f x ≠ f x
⊢ x ∈ ⊥

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
i j : β
h : i ≠ j
u : Finset α
hi : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) i
hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) j
x : α
hx : x ∈ u
⊢ x ∈ ⊥

Tactic:
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx

Result:
case intro
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Set β
t : Finset α
j : β
u : Finset α
hj : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) j
x : α
hx : x ∈ u
h : f x ≠ j
hi : u ≤ (fun x => filter (fun x_1 => f x_1 = x) t) (f x)
⊢ x ∈ ⊥
-- Mathlib/Computability/PartrecCode.lean
theorem eval_eq_rfindOpt (c n) : eval c n = Nat.rfindOpt fun k => evaln k c n :=
  Part.ext fun x => by
    refine evaln_complete.trans (Nat.rfindOpt_mono ?_).symm
    intro a m n hl; apply evaln_mono hl

Proof state:
c : Code
n✝ x a m n : ℕ
hl : m ≤ n
⊢ a ∈ evaln m c n✝ → a ∈ evaln n c n✝

Tactic:
apply evaln_mono hl

Result:
no goals

Proof state:
c : Code
n x : ℕ
⊢ x ∈ c.eval n ↔ x ∈ rfindOpt fun k => evaln k c n

Tactic:
refine evaln_complete.trans (Nat.rfindOpt_mono ?_).symm

Result:
c : Code
n x : ℕ
⊢ ∀ {a m n_1 : ℕ}, m ≤ n_1 → a ∈ evaln m c n → a ∈ evaln n_1 c n

Proof state:
c : Code
n x : ℕ
⊢ ∀ {a m n_1 : ℕ}, m ≤ n_1 → a ∈ evaln m c n → a ∈ evaln n_1 c n

Tactic:
intro a m n hl

Result:
c : Code
n✝ x a m n : ℕ
hl : m ≤ n
⊢ a ∈ evaln m c n✝ → a ∈ evaln n c n✝