harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
/-- If the (coproduct-like) biproduct comparison for `F` and `f` is an epimorphism, then `F`
    preserves the biproduct of `F` and `f`. For the converse, see `mapBiproduct`. -/
lemma preservesBiproduct_of_epi_biproductComparison' {f : J → C} [HasBiproduct f]
    [HasBiproduct (F.obj ∘ f)] [Epi (biproductComparison' F f)] : PreservesBiproduct f F

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type
inst✝³ : Fintype J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
⊢ Epi (F.splitEpiBiproductComparison f).section_

Tactic:
simpa

Result:
no goals

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type
inst✝³ : Fintype J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
⊢ PreservesBiproduct f F

Tactic:
haveI : Epi (splitEpiBiproductComparison F f).section_ := by simpa

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type
inst✝³ : Fintype J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
this : Epi (F.splitEpiBiproductComparison f).section_
⊢ PreservesBiproduct f F

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type
inst✝³ : Fintype J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
this : Epi (F.splitEpiBiproductComparison f).section_
⊢ PreservesBiproduct f F

Tactic:
haveI : IsIso (biproductComparison F f) :=
  IsIso.of_epi_section' (splitEpiBiproductComparison F f)

Result:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type
inst✝³ : Fintype J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
this✝ : Epi (F.splitEpiBiproductComparison f).section_
this : IsIso (F.biproductComparison f)
⊢ PreservesBiproduct f F

Proof state:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Preadditive C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.PreservesZeroMorphisms
J : Type
inst✝³ : Fintype J
f : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct (F.obj ∘ f)
inst✝ : Epi (F.biproductComparison' f)
this✝ : Epi (F.splitEpiBiproductComparison f).section_
this : IsIso (F.biproductComparison f)
⊢ PreservesBiproduct f F

Tactic:
apply preservesBiproduct_of_mono_biproductComparison

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem div_int (h : Irrational x) {m : ℤ} (hm : m ≠ 0) : Irrational (x / m)

Proof state:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0

Tactic:
rwa [Int.cast_ne_zero]

Result:
no goals

Proof state:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)

Tactic:
refine h.div_rat ?_

Result:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ ↑m ≠ 0

Proof state:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑m)

Tactic:
rw [← cast_intCast]

Result:
x : ℝ
h : Irrational x
m : ℤ
hm : m ≠ 0
⊢ Irrational (x / ↑↑m)
-- Mathlib/Data/Finset/Sym.lean
theorem sym2_eq_empty : s.sym2 = ∅ ↔ s = ∅

Proof state:
α : Type u_1
s : Finset α
⊢ s.sym2 = ∅ ↔ s = ∅

Tactic:
rw [← val_eq_zero, sym2_val, Multiset.sym2_eq_zero_iff, val_eq_zero]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_range_div (n : ℕ) (f : ℕ → G) :
    ((range n).map fun k ↦ f (k + 1) / f k).prod = f n / f 0

Proof state:
case h
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
x✝ : ℕ
⊢ ((fun x => x⁻¹) ∘ fun k => f (k + 1) / f k) x✝ = f x✝ / f (x✝ + 1)

Tactic:
apply inv_div

Result:
no goals

Proof state:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
⊢ ((fun x => x⁻¹) ∘ fun k => f (k + 1) / f k) = fun k => f k / f (k + 1)

Tactic:
ext

Result:
case h
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
x✝ : ℕ
⊢ ((fun x => x⁻¹) ∘ fun k => f (k + 1) / f k) x✝ = f x✝ / f (x✝ + 1)

Proof state:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
h : ((fun x => x⁻¹) ∘ fun k => f (k + 1) / f k) = fun k => f k / f (k + 1)
⊢ (map (fun k => f (k + 1) / f k) (range n)).prod = f n / f 0

Tactic:
rw [← inv_inj, prod_inv, map_map, inv_div, h, prod_range_div']

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma leftShift_zero (a n' : ℤ) (hn' : n + a = n') :
    (0 : Cochain K L n).leftShift a n' hn' = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n + a = n'
⊢ leftShift 0 a n' hn' = 0

Tactic:
change leftShiftAddEquiv K L n a n' hn' 0 = 0

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn') 0 = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn') 0 = 0

Tactic:
apply _root_.map_zero

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Basic.lean
theorem coe_ringOfIntegersEquiv (z : 𝓞 ℚ) :
    (Rat.ringOfIntegersEquiv z : ℚ) = algebraMap (𝓞 ℚ) ℚ z

Proof state:
case intro
z : ℤ
⊢ ↑(ringOfIntegersEquiv (ringOfIntegersEquiv.symm z)) = (algebraMap (𝓞 ℚ) ℚ) (ringOfIntegersEquiv.symm z)

Tactic:
simp

Result:
no goals

Proof state:
z : 𝓞 ℚ
⊢ ↑(ringOfIntegersEquiv z) = (algebraMap (𝓞 ℚ) ℚ) z

Tactic:
obtain ⟨z, rfl⟩ := Rat.ringOfIntegersEquiv.symm.surjective z

Result:
case intro
z : ℤ
⊢ ↑(ringOfIntegersEquiv (ringOfIntegersEquiv.symm z)) = (algebraMap (𝓞 ℚ) ℚ) (ringOfIntegersEquiv.symm z)
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem isBigO_at_im_infty_jacobiTheta_sub_one :
    (fun τ => jacobiTheta τ - 1) =O[comap im atTop] fun τ => rexp (-π * τ.im)

Proof state:
⊢ ∃ c a, ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖

Tactic:
refine ⟨2 / (1 - rexp (-(π * 1))), 1, fun y hy τ hτ =>
  (norm_jacobiTheta_sub_one_le (hτ.symm ▸ zero_lt_one.trans_le hy : 0 < im τ)).trans ?_⟩

Result:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖

Proof state:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))

Tactic:
gcongr

Result:
case h.hc
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 0 < 1 - rexp (-(π * 1))

Proof state:
case h.hc
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 0 < 1 - rexp (-(π * 1))

Tactic:
simp [pi_pos]

Result:
no goals

Proof state:
⊢ (fun τ => jacobiTheta τ - 1) =O[comap im atTop] fun τ => rexp (-π * τ.im)

Tactic:
simp_rw [IsBigO, IsBigOWith, Filter.eventually_comap, Filter.eventually_atTop]

Result:
⊢ ∃ c a, ∀ b ≥ a, ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖

Proof state:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖

Tactic:
rw [Real.norm_eq_abs, Real.abs_exp, hτ, neg_mul]

Result:
y : ℝ
hy : y ≥ 1
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))
-- Mathlib/Algebra/Quandle.lean
theorem conj_swap {G : Type*} [Group G] (x y : Conj G) : x ◃ y = y ↔ y ◃ x = x

Proof state:
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y ↔ y * x * y⁻¹ = x

Tactic:
constructor

Result:
case mp
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y → y * x * y⁻¹ = x

case mpr
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y

Proof state:
case mpr
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y

Tactic:
intro h

Result:
case mpr
G : Type u_2
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
⊢ x * y * x⁻¹ = y

Proof state:
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x ◃ y = y ↔ y ◃ x = x

Tactic:
dsimp [Conj] at *

Result:
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y ↔ y * x * y⁻¹ = x

Proof state:
case mp
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ x * y * x⁻¹ = y → y * x * y⁻¹ = x

case mpr
G : Type u_2
inst✝ : Group G
x y : Conj G
⊢ y * x * y⁻¹ = x → x * y * x⁻¹ = y

Tactic:
repeat' intro h; conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp

Result:
no goals

Proof state:
case mpr
G : Type u_2
inst✝ : Group G
x y : Conj G
h : y * x * y⁻¹ = x
⊢ x * y * x⁻¹ = y

Tactic:
conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem add_quot {a b} : (⟨Quot.mk _ a⟩ + ⟨Quot.mk _ b⟩ : RingQuot r) = ⟨Quot.mk _ (a + b)⟩

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ RingQuot.add r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a + b) }

Tactic:
rw [add_def]

Result:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ (match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with
    | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x1 x2 => x1 + x2) ⋯ ⋯ a b }) =
    { toQuot := Quot.mk (Rel r) (a + b) }

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ { toQuot := Quot.mk (Rel r) a } + { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a + b) }

Tactic:
show add r _ _ = _

Result:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ RingQuot.add r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a + b) }

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
a b : R
⊢ (match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with
    | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ (fun x1 x2 => x1 + x2) ⋯ ⋯ a b }) =
    { toQuot := Quot.mk (Rel r) (a + b) }

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_lt_pi_div_two {x : ℝ} : arccos x < π / 2 ↔ 0 < x

Proof state:
x : ℝ
⊢ arccos x < π / 2 ↔ 0 < x

Tactic:
simp [arccos]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem _root_.Set.measure_eq_iInf_isOpen (A : Set α) (μ : Measure α) [OuterRegular μ] :
    μ A = ⨅ (U : Set α) (_ : A ⊆ U) (_ : IsOpen U), μ U

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
⊢ ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U ≤ μ A

Tactic:
refine le_of_forall_lt' fun r hr => ?_

Result:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
r : ℝ≥0∞
hr : μ A < r
⊢ ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U < r

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
r : ℝ≥0∞
hr : μ A < r
⊢ ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U < r

Tactic:
simpa only [iInf_lt_iff, exists_prop] using A.exists_isOpen_lt_of_lt r hr

Result:
no goals

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
⊢ μ A = ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U

Tactic:
refine le_antisymm (le_iInf₂ fun s hs => le_iInf fun _ => μ.mono hs) ?_

Result:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
A : Set α
μ : Measure α
inst✝ : μ.OuterRegular
⊢ ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), μ U ≤ μ A
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem mkImpCached_le_size (aig : AIG α) (input : BinaryInput aig) :
    aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)

Result:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false true)).aig.decls.size

Proof state:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkGateCached (input.asGateInput false true)).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ (aig.mkImpCached input).aig.decls.size

Tactic:
simp only [mkImpCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.mkGateCached
            {
              lhs :=
                { ref := ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).ref, inv := false },
              rhs :=
                { ref := (aig.mkGateCached (input.asGateInput false true)).ref.cast ⋯, inv := true } }).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤
    (((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.mkGateCached
            {
              lhs :=
                { ref := ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).ref, inv := false },
              rhs :=
                { ref := (aig.mkGateCached (input.asGateInput false true)).ref.cast ⋯, inv := true } }).aig.decls.size

Tactic:
apply LawfulOperator.le_size_of_le_aig_size

Result:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ ((aig.mkGateCached (input.asGateInput false true)).aig.mkConstCached true).aig.decls.size

Proof state:
case h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.BinaryInput
⊢ aig.decls.size ≤ aig.decls.size

Tactic:
omega

Result:
no goals
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_singleton (x : ZFSet) : rank {x} = succ (rank x) :=
  (rank_insert _ _).trans (by simp)

Proof state:
x : ZFSet.{u_1}
⊢ succ x.rank ⊔ ∅.rank = succ x.rank

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
theorem add_eq_coe :
    ∀ {a b : WithBot α} {c : α}, a + b = c ↔ ∃ a' b' : α, ↑a' = a ∧ ↑b' = b ∧ a' + b' = c
  | ⊥, b, c => by simp
  | some a, ⊥, c => by simp
  | some a, some b, c => by norm_cast; simp

Proof state:
α : Type u
inst✝ : Add α
a b c : α
⊢ ↑a + ↑b = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ↑b ∧ a' + b' = c

Tactic:
norm_cast

Result:
α : Type u
inst✝ : Add α
a b c : α
⊢ a + b = c ↔ ∃ a' b', a' = a ∧ b' = b ∧ a' + b' = c

Proof state:
α : Type u
inst✝ : Add α
a b c : α
⊢ a + b = c ↔ ∃ a' b', a' = a ∧ b' = b ∧ a' + b' = c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : Add α
b : WithBot α
c : α
⊢ ⊥ + b = ↑c ↔ ∃ a' b', ↑a' = ⊥ ∧ ↑b' = b ∧ a' + b' = c

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝ : Add α
a c : α
⊢ ↑a + ⊥ = ↑c ↔ ∃ a' b', ↑a' = ↑a ∧ ↑b' = ⊥ ∧ a' + b' = c

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
lemma girth_eq_zero : G.girth = 0 ↔ G.IsAcyclic :=
  ⟨fun h ↦ not_not.mp <| three_le_girth.mt <| by omega, fun h ↦ by simp [girth, h]⟩

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.girth = 0
⊢ ¬3 ≤ G.girth

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.IsAcyclic
⊢ G.girth = 0

Tactic:
simp [girth, h]

Result:
no goals
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@[simp]
lemma left_top_iff :
    p.IsPerfectCompl ⊤ V ↔ V = ⊤

Proof state:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : p.IsPerfectCompl ⊤ V
⊢ V = ⊤

Tactic:
exact eq_top_of_isCompl_bot <| by simpa using h.isCompl_right

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : V = ⊤
⊢ IsCompl ⊤ (Submodule.map p.toDualLeft.symm ⊤.dualAnnihilator)

Tactic:
simpa using isCompl_top_bot

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : p.IsPerfectCompl ⊤ V
⊢ IsCompl V ⊥

Tactic:
simpa using h.isCompl_right

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ ⊤

Tactic:
exact
  { isCompl_left := by simpa using isCompl_top_bot
    isCompl_right := by simpa using isCompl_top_bot }

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
⊢ p.IsPerfectCompl ⊤ V ↔ V = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : p.IsPerfectCompl ⊤ V
⊢ V = ⊤

case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ V

Proof state:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ V

Tactic:
rw [h]

Result:
case refine_2
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : V = ⊤
⊢ p.IsPerfectCompl ⊤ ⊤

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
p : PerfectPairing R M N
V : Submodule R N
h : V = ⊤
⊢ IsCompl ⊤ (Submodule.map p.toDualRight.symm ⊤.dualAnnihilator)

Tactic:
simpa using isCompl_top_bot

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem deriv_const_mul_field (u : 𝕜') : deriv (fun y => u * v y) x = u * deriv v x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
⊢ deriv (fun y => u * v y) x = u * deriv v x

Tactic:
simp only [mul_comm u, deriv_mul_const_field]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem fastLegendreSym.eq : legendreSym = fastLegendreSym

Proof state:
⊢ legendreSym = fastLegendreSym

Tactic:
ext p _ a

Result:
case h.h.h
p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = fastLegendreSym p a

Proof state:
case h.h.h
p : ℕ
x✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = fastLegendreSym p a

Tactic:
rw [legendreSym.to_jacobiSym, fastLegendreSym]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem tan_eq_of_two_nsmul_eq {θ ψ : Angle} (h : (2 : ℕ) • θ = (2 : ℕ) • ψ) : tan θ = tan ψ

Proof state:
case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan

Tactic:
exact tan_add_pi _

Result:
no goals

Proof state:
θ ψ : Angle
h : 2 • θ = 2 • ψ
⊢ θ.tan = ψ.tan

Tactic:
rw [two_nsmul_eq_iff] at h

Result:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ θ.tan = ψ.tan

Proof state:
case inl
θ : Angle
⊢ θ.tan = θ.tan

Tactic:
rfl

Result:
no goals

Proof state:
θ ψ : Angle
h : θ = ψ ∨ θ = ψ + ↑π
⊢ θ.tan = ψ.tan

Tactic:
rcases h with (rfl | rfl)

Result:
case inl
θ : Angle
⊢ θ.tan = θ.tan

case inr
ψ : Angle
⊢ (ψ + ↑π).tan = ψ.tan
-- Mathlib/Topology/Basic.lean
theorem compl_frontier_eq_union_interior :
    (frontier s)ᶜ = interior s ∪ interior sᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ (frontier s)ᶜ = interior s ∪ interior sᶜ

Tactic:
rw [frontier_eq_inter_compl_interior]

Result:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ ((interior s)ᶜ ∩ (interior sᶜ)ᶜ)ᶜ = interior s ∪ interior sᶜ

Tactic:
simp only [compl_inter, compl_compl]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem map_inv_of_isMulOneCocycle {f : G → M} (hf : IsMulOneCocycle f) (g : G) :
    g • f g⁻¹ = (f g)⁻¹

Proof state:
G : Type u_1
M : Type u_2
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulAction G M
f : G → M
hf : IsMulOneCocycle f
g : G
⊢ g • f g⁻¹ = (f g)⁻¹

Tactic:
rw [← mul_eq_one_iff_eq_inv, ← map_one_of_isMulOneCocycle hf, ← mul_inv_cancel g, hf g g⁻¹]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem isTorsion'_iff_torsion'_eq_top : IsTorsion' M S ↔ torsion' R M S = ⊤ :=
  ⟨fun h => eq_top_iff.mpr fun _ _ => @h _, fun h x => by
    rw [← @mem_torsion'_iff R, h]
    trivial⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ ∃ a, a • x = 0

Tactic:
rw [← @mem_torsion'_iff R, h]

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ x ∈ ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_3
inst✝² : CommMonoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
h : torsion' R M S = ⊤
x : M
⊢ x ∈ ⊤

Tactic:
trivial

Result:
no goals