harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Floor.lean
theorem subsingleton_floorRing {α} [LinearOrderedRing α] : Subsingleton (FloorRing α)

Proof state:
case mk.mk
α : Type u_4
inst✝ : LinearOrderedRing α
floor✝¹ ceil✝¹ : α → ℤ
gc_coe_floor✝¹ : GaloisConnection Int.cast floor✝¹
gc_ceil_coe✝¹ : GaloisConnection ceil✝¹ Int.cast
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝¹, ceil := ceil✝¹, gc_coe_floor := gc_coe_floor✝¹, gc_ceil_coe := gc_ceil_coe✝¹ } =
    { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ }

Tactic:
congr

Result:
no goals

Proof state:
α : Type u_4
inst✝ : LinearOrderedRing α
⊢ Subsingleton (FloorRing α)

Tactic:
refine ⟨fun H₁ H₂ => ?_⟩

Result:
α : Type u_4
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
⊢ H₁ = H₂

Proof state:
α : Type u_4
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this : FloorRing.floor = FloorRing.floor
⊢ H₁ = H₂

Tactic:
have : H₁.ceil = H₂.ceil := funext fun a => (H₁.gc_ceil_coe.l_unique H₂.gc_ceil_coe) fun _ => rfl

Result:
α : Type u_4
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ H₁ = H₂

Proof state:
case mk
α : Type u_4
inst✝ : LinearOrderedRing α
H₂ : FloorRing α
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ } = H₂

Tactic:
cases H₂

Result:
case mk.mk
α : Type u_4
inst✝ : LinearOrderedRing α
floor✝¹ ceil✝¹ : α → ℤ
gc_coe_floor✝¹ : GaloisConnection Int.cast floor✝¹
gc_ceil_coe✝¹ : GaloisConnection ceil✝¹ Int.cast
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝¹, ceil := ceil✝¹, gc_coe_floor := gc_coe_floor✝¹, gc_ceil_coe := gc_ceil_coe✝¹ } =
    { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ }

Proof state:
α : Type u_4
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ H₁ = H₂

Tactic:
cases H₁

Result:
case mk
α : Type u_4
inst✝ : LinearOrderedRing α
H₂ : FloorRing α
floor✝ ceil✝ : α → ℤ
gc_coe_floor✝ : GaloisConnection Int.cast floor✝
gc_ceil_coe✝ : GaloisConnection ceil✝ Int.cast
this✝ : FloorRing.floor = FloorRing.floor
this : FloorRing.ceil = FloorRing.ceil
⊢ { floor := floor✝, ceil := ceil✝, gc_coe_floor := gc_coe_floor✝, gc_ceil_coe := gc_ceil_coe✝ } = H₂

Proof state:
α : Type u_4
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
⊢ H₁ = H₂

Tactic:
have : H₁.floor = H₂.floor :=
  funext fun a => (H₁.gc_coe_floor.u_unique H₂.gc_coe_floor) fun _ => rfl

Result:
α : Type u_4
inst✝ : LinearOrderedRing α
H₁ H₂ : FloorRing α
this : FloorRing.floor = FloorRing.floor
⊢ H₁ = H₂
-- Mathlib/Data/Nat/Prime/Basic.lean
theorem Prime.pow_eq_iff {p a k : ℕ} (hp : p.Prime) : a ^ k = p ↔ a = p ∧ k = 1

Proof state:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1

Tactic:
rw [← h, hp.eq_one_of_pow, eq_self_iff_true, _root_.and_true, pow_one]

Result:
no goals

Proof state:
p a k : ℕ
hp : Prime p
h : a = p ∧ k = 1
⊢ a ^ k = p

Tactic:
rw [h.1, h.2, pow_one]

Result:
no goals

Proof state:
p a k : ℕ
hp : Prime p
⊢ a ^ k = p ↔ a = p ∧ k = 1

Tactic:
refine ⟨fun h => ?_, fun h => by rw [h.1, h.2, pow_one]⟩

Result:
p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ a = p ∧ k = 1

Proof state:
p a k : ℕ
hp : Prime p
h : a ^ k = p
⊢ a = p ∧ k = 1

Tactic:
rw [← h] at hp

Result:
p a k : ℕ
hp : Prime (a ^ k)
h : a ^ k = p
⊢ a = p ∧ k = 1
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.sphere_zero_eq {n : Type*} [Fintype n] (r : ℝ) (hr : 0 ≤ r) :
    Metric.sphere (0 : EuclideanSpace ℝ n) r = {x | ∑ i, x i ^ 2 = r ^ 2}

Proof state:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i : n, x i ^ 2
⊢ x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 = r ^ 2}

Tactic:
simp_rw [mem_setOf, mem_sphere_zero_iff_norm, norm_eq, norm_eq_abs, sq_abs,
  Real.sqrt_eq_iff_eq_sq this hr]

Result:
no goals

Proof state:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
⊢ x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 = r ^ 2}

Tactic:
have : (0 : ℝ) ≤ ∑ i, x i ^ 2 := Finset.sum_nonneg fun _ _ => sq_nonneg _

Result:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
this : 0 ≤ ∑ i : n, x i ^ 2
⊢ x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 = r ^ 2}

Proof state:
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
⊢ Metric.sphere 0 r = {x | ∑ i : n, x i ^ 2 = r ^ 2}

Tactic:
ext x

Result:
case h
n : Type u_7
inst✝ : Fintype n
r : ℝ
hr : 0 ≤ r
x : EuclideanSpace ℝ n
⊢ x ∈ Metric.sphere 0 r ↔ x ∈ {x | ∑ i : n, x i ^ 2 = r ^ 2}
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Complex.lean
theorem sin_eq_sin_iff {x y : ℂ} :
    sin x = sin y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = (2 * k + 1) * π - x

Proof state:
x y : ℂ
⊢ (∃ k, y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ∨ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2) ↔
    ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x

Tactic:
refine exists_congr fun k => or_congr ?_ ?_ <;> refine Eq.congr rfl ?_ <;> field_simp <;> ring

Result:
no goals

Proof state:
x y : ℂ
⊢ sin x = sin y ↔ ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x

Tactic:
simp only [← Complex.cos_sub_pi_div_two, cos_eq_cos_iff, sub_eq_iff_eq_add]

Result:
x y : ℂ
⊢ (∃ k, y = 2 * ↑k * ↑π + (x - ↑π / 2) + ↑π / 2 ∨ y = 2 * ↑k * ↑π - (x - ↑π / 2) + ↑π / 2) ↔
    ∃ k, y = 2 * ↑k * ↑π + x ∨ y = (2 * ↑k + 1) * ↑π - x
-- Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
theorem HasProd.unique {a₁ a₂ : α} [T2Space α] : HasProd f a₁ → HasProd f a₂ → a₁ = a₂

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a₁ a₂ : α
inst✝ : T2Space α
⊢ HasProd f a₁ → HasProd f a₂ → a₁ = a₂

Tactic:
exact tendsto_nhds_unique

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : CommMonoid α
inst✝¹ : TopologicalSpace α
f : β → α
a₁ a₂ : α
inst✝ : T2Space α
⊢ HasProd f a₁ → HasProd f a₂ → a₁ = a₂

Tactic:
classical exact tendsto_nhds_unique

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_mul_I : sin (x * I) = sinh x * I

Proof state:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I

Tactic:
rw [← neg_neg (sinh x), ← h]

Result:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I

Proof state:
x : ℂ
⊢ sinh (x * I * I) = -sinh x

Tactic:
ring_nf

Result:
x : ℂ
⊢ sinh (x * I ^ 2) = -sinh x

Proof state:
x : ℂ
⊢ I * sin (x * I) = -sinh x

Tactic:
rw [mul_comm, ← sinh_mul_I]

Result:
x : ℂ
⊢ sinh (x * I * I) = -sinh x

Proof state:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I

Tactic:
apply Complex.ext <;> simp

Result:
no goals

Proof state:
x : ℂ
⊢ sin (x * I) = sinh x * I

Tactic:
have h : I * sin (x * I) = -sinh x := by
  rw [mul_comm, ← sinh_mul_I]
  ring_nf
  simp

Result:
x : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I

Proof state:
x : ℂ
⊢ sinh (x * I ^ 2) = -sinh x

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/CondDistrib.lean
theorem _root_.MeasureTheory.Integrable.integral_norm_condDistrib_map
    (hY : AEMeasurable Y μ) (hf_int : Integrable f (μ.map fun a => (X a, Y a))) :
    Integrable (fun x => ∫ y, ‖f (x, y)‖ ∂condDistrib Y X μ x) (μ.map X)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x)
    (Measure.map (fun a => (X a, Y a)) μ).fst

Tactic:
exact hf_int.integral_norm_condKernel

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(condDistrib Y X μ) x) (Measure.map X μ)

Tactic:
rw [condDistrib, ← Measure.fst_map_prod_mk₀ (X := X) hY]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a => (X a, Y a)) μ)
⊢ Integrable (fun x => ∫ (y : Ω), ‖f (x, y)‖ ∂(Measure.map (fun a => (X a, Y a)) μ).condKernel x)
    (Measure.map (fun a => (X a, Y a)) μ).fst
-- Mathlib/Data/Nat/Factorial/SuperFactorial.lean
theorem matrixOf_eval_descPochhammer_eq_mul_matrixOf_choose {n : ℕ} (v : Fin n → ℕ) :
    (Matrix.of (fun (i j : Fin n) => (descPochhammer ℤ j).eval (v i : ℤ))).det =
    (∏ i : Fin n, Nat.factorial i) *
      (Matrix.of (fun (i j : Fin n) => (Nat.choose (v i) (j : ℕ) : ℤ))).det

Proof state:
case h.e'_2.h.e'_6.h.e'_6.h.h
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ ↑((v x✝¹).descFactorial ↑x✝) = ↑(↑x✝)! * ↑((v x✝¹).choose ↑x✝)

Tactic:
congr

Result:
case h.e'_2.h.e'_6.h.e'_6.h.h.e_a
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ (v x✝¹).descFactorial ↑x✝ = (↑x✝)! * (v x✝¹).choose ↑x✝

Proof state:
case h.e'_2.h.e'_6.h.e'_6.h.h
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ Polynomial.eval (↑(v x✝¹)) (descPochhammer ℤ ↑x✝) = ↑(↑x✝)! * Matrix.of (fun i j => ↑((v i).choose ↑j)) x✝¹ x✝

Tactic:
rw [Matrix.of_apply, descPochhammer_eval_eq_descFactorial ℤ _ _]

Result:
case h.e'_2.h.e'_6.h.e'_6.h.h
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ ↑((v x✝¹).descFactorial ↑x✝) = ↑(↑x✝)! * ↑((v x✝¹).choose ↑x✝)

Proof state:
case h.e'_2.h.e'_6.h.e'_6.h.h.e_a
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ (v x✝¹).descFactorial ↑x✝ = (↑x✝)! * (v x✝¹).choose ↑x✝

Tactic:
exact Nat.descFactorial_eq_factorial_mul_choose _ _

Result:
no goals

Proof state:
case h.e'_3.h.e'_5
n : ℕ
v : Fin n → ℕ
⊢ ↑(∏ i : Fin n, (↑i)!) = ∏ i : Fin n, ↑(↑i)!

Tactic:
rw [Nat.cast_prod]

Result:
no goals

Proof state:
n : ℕ
v : Fin n → ℕ
⊢ (Matrix.of fun i j => Polynomial.eval (↑(v i)) (descPochhammer ℤ ↑j)).det =
    ↑(∏ i : Fin n, (↑i)!) * (Matrix.of fun i j => ↑((v i).choose ↑j)).det

Tactic:
convert Matrix.det_mul_row (fun (i : Fin n) => ((Nat.factorial (i : ℕ)) : ℤ)) _

Result:
case h.e'_2.h.e'_6.h.e'_6.h.h
n : ℕ
v : Fin n → ℕ
x✝¹ x✝ : Fin n
⊢ Polynomial.eval (↑(v x✝¹)) (descPochhammer ℤ ↑x✝) = ↑(↑x✝)! * Matrix.of (fun i j => ↑((v i).choose ↑j)) x✝¹ x✝

case h.e'_3.h.e'_5
n : ℕ
v : Fin n → ℕ
⊢ ↑(∏ i : Fin n, (↑i)!) = ∏ i : Fin n, ↑(↑i)!
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem exists_sSupIndep_sSup_simples_eq_top :
    ∃ s : Set (Submodule R M), sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R m

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
this : sSup {m | IsAtom m} = ⊤
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsAtom m

Tactic:
exact exists_sSupIndep_of_sSup_atoms_eq_top this

Result:
no goals

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m

Tactic:
have := sSup_simples_eq_top R M

Result:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
this : sSup {m | IsSimpleModule R ↥m} = ⊤
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m

Proof state:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
this : sSup {m | IsSimpleModule R ↥m} = ⊤
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m

Tactic:
simp_rw [isSimpleModule_iff_isAtom] at this ⊢

Result:
R : Type u_2
inst✝³ : Ring R
M : Type u_4
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
this : sSup {m | IsAtom m} = ⊤
⊢ ∃ s, sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsAtom m
-- Mathlib/Data/Set/Function.lean
theorem eqOn_piecewise {f f' g : α → β} {t} :
    EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

Tactic:
by_cases a ∈ s <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ (∀ ⦃x : α⦄, x ∈ t → s.piecewise f f' x = g x) ↔ ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)

Tactic:
refine forall_congr' fun a => ?_

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
a : α
⊢ a ∈ t → s.piecewise f f' a = g a ↔ (a ∈ t ∩ s → f a = g a) ∧ (a ∈ t ∩ sᶜ → f' a = g a)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ EqOn (s.piecewise f f') g t ↔ EqOn f g (t ∩ s) ∧ EqOn f' g (t ∩ sᶜ)

Tactic:
simp only [EqOn, ← forall_and]

Result:
α : Type u_1
β : Type u_2
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
f f' g : α → β
t : Set α
⊢ (∀ ⦃x : α⦄, x ∈ t → s.piecewise f f' x = g x) ↔ ∀ (x : α), (x ∈ t ∩ s → f x = g x) ∧ (x ∈ t ∩ sᶜ → f' x = g x)
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioo_succ_right_eq_Ioc (a b : α) : Ioo a (succ b) = Ioc a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a b : α
⊢ ↑(Ioo a (succ b)) = ↑(Ioc a b)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_iff_isIso_imageToKernel : S.Exact ↔ IsIso (imageToKernel S.f S.g S.zero)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel S.f S.g ⋯) ↔ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel S.f S.g ⋯) → IsIso (imageToKernel S.f S.g ⋯)

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) → Epi (imageToKernel S.f S.g ⋯)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel S.f S.g ⋯) → IsIso (imageToKernel S.f S.g ⋯)

Tactic:
intro

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : Epi (imageToKernel S.f S.g ⋯)
⊢ IsIso (imageToKernel S.f S.g ⋯)

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : Epi (imageToKernel S.f S.g ⋯)
⊢ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
apply isIso_of_mono_of_epi

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ Epi (imageToKernel S.f S.g ⋯)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) → Epi (imageToKernel S.f S.g ⋯)

Tactic:
intro

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ Epi (imageToKernel S.f S.g ⋯)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_imageToKernel]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (imageToKernel S.f S.g ⋯) ↔ IsIso (imageToKernel S.f S.g ⋯)
-- Mathlib/Data/Set/NAry.lean
theorem image_image2_distrib_right {g : γ → δ} {f' : α → β' → δ} {g' : β → β'}
    (h_distrib : ∀ a b, g (f a b) = f' a (g' b)) :
    (image2 f s t).image g = image2 f' s (t.image g') :=
  (image_image2_distrib h_distrib).trans <| by rw [image_id']

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ image2 f' ((fun a => a) '' s) (g' '' t) = image2 f' s (g' '' t)

Tactic:
rw [image_id']

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma zero_comp {n₁ n₂ n₁₂ : ℤ} (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : (0 : Cochain F G n₁).comp z₂ h = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (comp 0 z₂ h).v p q hpq = v 0 p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), zero_v, zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ comp 0 z₂ h = 0

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ (comp 0 z₂ h).v p q hpq = v 0 p q hpq
-- Mathlib/Topology/Homeomorph.lean
theorem self_trans_symm (h : X ≃ₜ Y) : h.trans h.symm = Homeomorph.refl X

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
⊢ h.trans h.symm = Homeomorph.refl X

Tactic:
ext

Result:
case H
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x✝ : X
⊢ (h.trans h.symm) x✝ = (Homeomorph.refl X) x✝

Proof state:
case H
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
x✝ : X
⊢ (h.trans h.symm) x✝ = (Homeomorph.refl X) x✝

Tactic:
apply symm_apply_apply

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem inf_principal_eq_bot {f : Filter α} {s : Set α} : f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f

Proof state:
α : Type u
f : Filter α
s : Set α
⊢ f ⊓ 𝓟 s = ⊥ ↔ sᶜ ∈ f

Tactic:
rw [← empty_mem_iff_bot, mem_inf_principal]

Result:
α : Type u
f : Filter α
s : Set α
⊢ {x | x ∈ s → x ∈ ∅} ∈ f ↔ sᶜ ∈ f

Proof state:
α : Type u
f : Filter α
s : Set α
⊢ {x | x ∈ s → x ∈ ∅} ∈ f ↔ sᶜ ∈ f

Tactic:
simp only [mem_empty_iff_false, imp_false, compl_def]

Result:
no goals
-- Mathlib/RingTheory/PiTensorProduct.lean
protected lemma mul_comm (x y : ⨂[R] i, A i) : mul x y = mul y x

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x y : ⨂[R] (i : ι), A i
⊢ mul = mul.flip

Tactic:
ext x y

Result:
case H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x✝ y✝ : ⨂[R] (i : ι), A i
x y : (i : ι) → A i
⊢ (((mul.compMultilinearMap (tprod R)) x).compMultilinearMap (tprod R)) y =
    (((mul.flip.compMultilinearMap (tprod R)) x).compMultilinearMap (tprod R)) y

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x y : ⨂[R] (i : ι), A i
⊢ (mul x) y = (mul y) x

Tactic:
suffices mul (R := R) (A := A) = mul.flip from
  DFunLike.congr_fun (DFunLike.congr_fun this x) y

Result:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x y : ⨂[R] (i : ι), A i
⊢ mul = mul.flip

Proof state:
case H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x✝ y✝ : ⨂[R] (i : ι), A i
x y : (i : ι) → A i
⊢ (mul ((tprod R) x)) ((tprod R) y) = (mul ((tprod R) y)) ((tprod R) x)

Tactic:
simp only [mul_tprod_tprod, mul_tprod_tprod, mul_comm x y]

Result:
no goals

Proof state:
case H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x✝ y✝ : ⨂[R] (i : ι), A i
x y : (i : ι) → A i
⊢ (((mul.compMultilinearMap (tprod R)) x).compMultilinearMap (tprod R)) y =
    (((mul.flip.compMultilinearMap (tprod R)) x).compMultilinearMap (tprod R)) y

Tactic:
dsimp

Result:
case H.H.H.H
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝² : CommSemiring R
inst✝¹ : (i : ι) → CommSemiring (A i)
inst✝ : (i : ι) → Algebra R (A i)
x✝ y✝ : ⨂[R] (i : ι), A i
x y : (i : ι) → A i
⊢ (mul ((tprod R) x)) ((tprod R) y) = (mul ((tprod R) y)) ((tprod R) x)
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem coe_eq_zero {x : Icc (0 : α) 1} : (x : α) = 0 ↔ x = 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ ↑x = 0 ↔ x = 0

Tactic:
symm

Result:
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 0 ↔ ↑x = 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
x : ↑(Icc 0 1)
⊢ x = 0 ↔ ↑x = 0

Tactic:
exact Subtype.ext_iff

Result:
no goals