harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Comma/Arrow.lean
theorem isIso_of_isIso_left_of_isIso_right {f g : Arrow T} (ff : f ⟶ g) [IsIso ff.left]
    [IsIso ff.right] : IsIso ff where
  out

Proof state:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ (𝟭 T).map (inv ff.left) ≫ f.hom = g.hom ≫ (𝟭 T).map (inv ff.right)

Tactic:
simp

Result:
no goals

Proof state:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := { left := inv ff.left, right := inv ff.right, w := ⋯ }
⊢ ff ≫ inverse = 𝟙 f ∧ inverse ≫ ff = 𝟙 g

Tactic:
aesop_cat

Result:
no goals

Proof state:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g

Tactic:
let inverse : g ⟶ f := ⟨inv ff.left, inv ff.right, (by simp)⟩

Result:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := { left := inv ff.left, right := inv ff.right, w := ⋯ }
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g

Proof state:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := { left := inv ff.left, right := inv ff.right, w := ⋯ }
⊢ ∃ inv, ff ≫ inv = 𝟙 f ∧ inv ≫ ff = 𝟙 g

Tactic:
apply Exists.intro inverse

Result:
T : Type u
inst✝² : Category.{v, u} T
f g : Arrow T
ff : f ⟶ g
inst✝¹ : IsIso ff.left
inst✝ : IsIso ff.right
inverse : g ⟶ f := { left := inv ff.left, right := inv ff.right, w := ⋯ }
⊢ ff ≫ inverse = 𝟙 f ∧ inverse ≫ ff = 𝟙 g
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_pi_Ico_toReal {a b : ι → ℝ} (h : a ≤ b) :
    (volume (pi univ fun i => Ico (a i) (b i))).toReal = ∏ i, (b i - a i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ (volume (univ.pi fun i => Ico (a i) (b i))).toReal = ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_pi_Ico, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- `bound` lemma for branching on `1 ≤ a ∨ a ≤ 1` when proving `a ^ n ≤ a ^ m` -/
@[bound]
lemma Bound.pow_le_pow_right_of_le_one_or_one_le (h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n) :
    a ^ n ≤ a ^ m

Proof state:
case inr.intro.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
m n : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
exact pow_le_pow_of_le_one a0 a1 mn

Result:
no goals

Proof state:
case inl.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
m n : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m

Tactic:
exact pow_right_mono₀ a1 nm

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
m n : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n
⊢ a ^ n ≤ a ^ m

Tactic:
obtain ⟨a1, nm⟩ | ⟨a0, a1, mn⟩ := h

Result:
case inl.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
m n : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m

case inr.intro.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
m n : ℕ
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma univ_infs_univ [Fintype α] : (univ : Finset α) ⊼ univ = univ

Proof state:
α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : SemilatticeInf α
inst✝ : Fintype α
⊢ univ ⊼ univ = univ

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_add_mul_left_left (m n k : ℕ) : gcd (m + n * k) n = gcd m n

Proof state:
m n k : ℕ
⊢ (m + n * k).gcd n = m.gcd n

Tactic:
rw [gcd_comm, gcd_add_mul_left_right, gcd_comm]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_reverse_noncomm : ∀ L : List G, L.reverse.prod = (L.map fun x => x⁻¹).prod⁻¹

Proof state:
G : Type u_7
inst✝ : Group G
⊢ ∀ (L : List G), L.reverse.prod = (map (fun x => x⁻¹) L).prod⁻¹

Tactic:
simp [prod_inv_reverse]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Invertible.lean
theorem invOf_div (a b : α) [Invertible a] [Invertible b] [Invertible (a / b)] :
    ⅟ (a / b) = b / a :=
  invOf_eq_right_inv (by simp [← mul_div_assoc])

Proof state:
α : Type u
inst✝³ : GroupWithZero α
a b : α
inst✝² : Invertible a
inst✝¹ : Invertible b
inst✝ : Invertible (a / b)
⊢ a / b * (b / a) = 1

Tactic:
simp [← mul_div_assoc]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lt_or_equiv_or_gf (x y : PGame) : x < y ∨ (x ≈ y) ∨ y ⧏ x

Proof state:
x y : PGame
⊢ x < y ∨ x ≈ y ∨ y ⧏ x

Tactic:
rw [lf_iff_lt_or_fuzzy, Fuzzy.swap_iff]

Result:
x y : PGame
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Proof state:
x y : PGame
⊢ x < y ∨ x ≈ y ∨ y < x ∨ x ‖ y

Tactic:
exact lt_or_equiv_or_gt_or_fuzzy x y

Result:
no goals
-- Mathlib/NumberTheory/JacobiSum/Basic.lean
/-- The Jacobi sum of two multiplicative characters on a nontrivial finite commutative ring `F`
can be written as a sum over `F \ {0,1}`. -/
lemma jacobiSum_eq_sum_sdiff (χ ψ : MulChar F R) :
    jacobiSum χ ψ = ∑ x ∈ univ \ {0,1}, χ x * ψ (1 - x)

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ jacobiSum χ ψ = ∑ x ∈ univ \ {0, 1}, χ x * ψ (1 - x)

Tactic:
simp only [jacobiSum, subset_univ, sum_sdiff_eq_sub, sub_eq_add_neg, self_eq_add_right,
  neg_eq_zero]

Result:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x ∈ {0, 1}, χ x * ψ (1 + -x) = 0

Proof state:
case h
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∀ x ∈ {0, 1}, χ x * ψ (1 + -x) = 0

Tactic:
simp only [mem_insert, mem_singleton, forall_eq_or_imp, χ.map_zero, neg_zero, add_zero, map_one,
  mul_one, forall_eq, add_neg_cancel, ψ.map_zero, mul_zero, and_self]

Result:
no goals

Proof state:
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∑ x ∈ {0, 1}, χ x * ψ (1 + -x) = 0

Tactic:
apply sum_eq_zero

Result:
case h
F : Type u_1
R : Type u_2
inst✝⁴ : CommRing F
inst✝³ : Nontrivial F
inst✝² : Fintype F
inst✝¹ : DecidableEq F
inst✝ : CommRing R
χ ψ : MulChar F R
⊢ ∀ x ∈ {0, 1}, χ x * ψ (1 + -x) = 0
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem integral_fn_integral_add ⦃f g : α × β → E⦄ (F : E → E') (hf : Integrable f (μ.prod ν))
    (hg : Integrable g (μ.prod ν)) :
    (∫ x, F (∫ y, f (x, y) + g (x, y) ∂ν) ∂μ) =
      ∫ x, F ((∫ y, f (x, y) ∂ν) + ∫ y, g (x, y) ∂ν) ∂μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ ∫ (x : α), F (∫ (y : β), f (x, y) + g (x, y) ∂ν) ∂μ =
    ∫ (x : α), F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν) ∂μ

Tactic:
refine integral_congr_ae ?_

Result:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (fun x => F (∫ (y : β), f (x, y) + g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν)

Proof state:
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
⊢ (fun x => F (∫ (y : β), f (x, y) + g (x, y) ∂ν)) =ᶠ[ae μ] fun x => F (∫ (y : β), f (x, y) ∂ν + ∫ (y : β), g (x, y) ∂ν)

Tactic:
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g

Result:
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y => f (a✝, y)) ν
h2g : Integrable (fun y => g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) + g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν + ∫ (y : β), g (a✝, y) ∂ν)

Proof state:
case h
α : Type u_1
β : Type u_2
E : Type u_3
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MeasurableSpace β
μ : Measure α
ν : Measure β
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : SFinite ν
inst✝³ : NormedSpace ℝ E
inst✝² : SFinite μ
E' : Type u_4
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f (μ.prod ν)
hg : Integrable g (μ.prod ν)
a✝ : α
h2f : Integrable (fun y => f (a✝, y)) ν
h2g : Integrable (fun y => g (a✝, y)) ν
⊢ F (∫ (y : β), f (a✝, y) + g (a✝, y) ∂ν) = F (∫ (y : β), f (a✝, y) ∂ν + ∫ (y : β), g (a✝, y) ∂ν)

Tactic:
simp [integral_add h2f h2g]

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem case_eval (f g) :
    (case f g).eval = fun v => v.headI.rec (f.eval v.tail) fun y _ => g.eval (y::v.tail)

Proof state:
f g : Code
⊢ (f.case g).eval = fun v => Nat.rec (f.eval v.tail) (fun y x => g.eval (y :: v.tail)) v.headI

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem range'_eq_singleton_iff {s n a : Nat} : range' s n = [a] ↔ s = a ∧ n = 1

Proof state:
s n a : Nat
⊢ range' s n = [a] ↔ s = a ∧ n = 1

Tactic:
rw [range'_eq_cons_iff]

Result:
s n a : Nat
⊢ s = a ∧ 0 < n ∧ [] = range' (a + 1) (n - 1) ↔ s = a ∧ n = 1

Proof state:
s n : Nat
⊢ 0 < n ∧ n - 1 = 0 ↔ n = 1

Tactic:
omega

Result:
no goals

Proof state:
s n a : Nat
⊢ s = a ∧ 0 < n ∧ [] = range' (a + 1) (n - 1) ↔ s = a ∧ n = 1

Tactic:
simp only [nil_eq, range'_eq_nil_iff, and_congr_right_iff]

Result:
s n a : Nat
⊢ s = a → (0 < n ∧ n - 1 = 0 ↔ n = 1)

Proof state:
s n a : Nat
⊢ s = a → (0 < n ∧ n - 1 = 0 ↔ n = 1)

Tactic:
rintro rfl

Result:
s n : Nat
⊢ 0 < n ∧ n - 1 = 0 ↔ n = 1
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem constr_comp (f : M' →ₗ[R] M') (v : ι → M') :
    constr (M' := M') b S (f ∘ v) = f.comp (constr (M' := M') b S v) :=
  b.ext fun i => by simp only [Basis.constr_basis, LinearMap.comp_apply, Function.comp]

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M'
b : Basis ι R M
S : Type u_10
inst✝² : Semiring S
inst✝¹ : Module S M'
inst✝ : SMulCommClass R S M'
f : M' →ₗ[R] M'
v : ι → M'
i : ι
⊢ ((b.constr S) (⇑f ∘ v)) (b i) = (f ∘ₗ (b.constr S) v) (b i)

Tactic:
simp only [Basis.constr_basis, LinearMap.comp_apply, Function.comp]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
lemma isPresentation_iff :
    solution.IsPresentation ↔
      Submodule.span A (Set.range solution.var) = ⊤ ∧
      LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.IsPresentation ↔
    Submodule.span A (Set.range solution.var) = ⊤ ∧
      LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

Tactic:
rw [← injective_fromQuotient_iff_ker_π_eq_span,
  ← surjective_π_iff_span_eq_top, ← surjective_fromQuotient_iff_surjective_π, ]

Result:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.IsPresentation ↔ Function.Surjective ⇑solution.fromQuotient ∧ Function.Injective ⇑solution.fromQuotient

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ solution.IsPresentation ↔ Function.Surjective ⇑solution.fromQuotient ∧ Function.Injective ⇑solution.fromQuotient

Tactic:
exact ⟨fun h ↦ ⟨h.bijective.2, h.bijective.1⟩, fun h ↦ ⟨⟨h.2, h.1⟩⟩⟩

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_eq_init {α : Fin (n + 1) → Sort*} (v : (i : Fin (n + 1)) → α i) :
    take n n.le_succ v = init v

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin n
⊢ v (castLE ⋯ i) = v i.castSucc

Tactic:
congr

Result:
no goals

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin n
⊢ take n ⋯ v i = init v i

Tactic:
simp only [Nat.succ_eq_add_one, take, init]

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin n
⊢ v (castLE ⋯ i) = v i.castSucc

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
⊢ take n ⋯ v = init v

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u_2
v : (i : Fin (n + 1)) → α i
i : Fin n
⊢ take n ⋯ v i = init v i
-- Mathlib/Order/Filter/Basic.lean
theorem eventually_congr {f : Filter α} {p q : α → Prop} (h : ∀ᶠ x in f, p x ↔ q x) :
    (∀ᶠ x in f, p x) ↔ ∀ᶠ x in f, q x :=
  ⟨fun hp => hp.congr h, fun hq => hq.congr <| by simpa only [Iff.comm] using h⟩

Proof state:
α : Type u
f : Filter α
p q : α → Prop
h : ∀ᶠ (x : α) in f, p x ↔ q x
hq : ∀ᶠ (x : α) in f, q x
⊢ ∀ᶠ (x : α) in f, q x ↔ p x

Tactic:
simpa only [Iff.comm] using h

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_exchange' {a b : α} (ha : a ∉ s) (hb : b ∈ s) :
    (insert a s \ {b}).ncard = s.ncard

Proof state:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a s \ {b}).ncard = s.ncard

Tactic:
rw [← ncard_exchange ha hb, ← singleton_union, ← singleton_union, union_diff_distrib,
  @diff_singleton_eq_self _ b {a} fun h ↦ ha (by rwa [← mem_singleton_iff.mp h])]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
h : b ∈ {a}
⊢ a ∈ s

Tactic:
rwa [← mem_singleton_iff.mp h]

Result:
no goals
-- Mathlib/Order/Hom/Basic.lean
theorem map_inv_le_iff (f : F) {a : α} {b : β} : EquivLike.inv f b ≤ a ↔ b ≤ f a

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ EquivLike.inv f b ≤ a ↔ b ≤ f a

Tactic:
convert (map_le_map_iff f (a := EquivLike.inv f b) (b := a)).symm

Result:
case h.e'_2.h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = f (EquivLike.inv f b)

Proof state:
case h.e'_2.h.e'_3
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LE α
inst✝² : LE β
inst✝¹ : EquivLike F α β
inst✝ : OrderIsoClass F α β
f : F
a : α
b : β
⊢ b = f (EquivLike.inv f b)

Tactic:
exact (EquivLike.right_inv f _).symm

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem ι_glueMorphisms {Y : Scheme} (f : ∀ x, 𝒰.obj x ⟶ Y)
    (hf : ∀ x y, pullback.fst (𝒰.map x) (𝒰.map y) ≫ f x = pullback.snd _ _ ≫ f y)
    (x : 𝒰.J) : 𝒰.map x ≫ 𝒰.glueMorphisms f hf = f x

Proof state:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.J) → 𝒰.obj x ⟶ Y
hf : ∀ (x y : 𝒰.J), pullback.fst (𝒰.map x) (𝒰.map y) ≫ f x = pullback.snd (𝒰.map x) (𝒰.map y) ≫ f y
x : 𝒰.J
⊢ 𝒰.map x ≫ glueMorphisms 𝒰 f hf = f x

Tactic:
rw [← ι_fromGlued, Category.assoc, glueMorphisms, IsIso.hom_inv_id_assoc]

Result:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.J) → 𝒰.obj x ⟶ Y
hf : ∀ (x y : 𝒰.J), pullback.fst (𝒰.map x) (𝒰.map y) ≫ f x = pullback.snd (𝒰.map x) (𝒰.map y) ≫ f y
x : 𝒰.J
⊢ (gluedCover 𝒰).ι x ≫ Multicoequalizer.desc (gluedCover 𝒰).diagram Y f ⋯ = f x

Proof state:
X : Scheme
𝒰 : X.OpenCover
Y : Scheme
f : (x : 𝒰.J) → 𝒰.obj x ⟶ Y
hf : ∀ (x y : 𝒰.J), pullback.fst (𝒰.map x) (𝒰.map y) ≫ f x = pullback.snd (𝒰.map x) (𝒰.map y) ≫ f y
x : 𝒰.J
⊢ (gluedCover 𝒰).ι x ≫ Multicoequalizer.desc (gluedCover 𝒰).diagram Y f ⋯ = f x

Tactic:
erw [Multicoequalizer.π_desc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem zero_fdiv (b : Int) : fdiv 0 b = 0

Proof state:
b : Int
⊢ fdiv 0 b = 0

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem Preconnected.set_univ_walk_nonempty (hconn : G.Preconnected) (u v : V) :
    (Set.univ : Set (G.Walk u v)).Nonempty

Proof state:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Nonempty (G.Walk u v)

Tactic:
exact hconn u v

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Set.univ.Nonempty

Tactic:
rw [← Set.nonempty_iff_univ_nonempty]

Result:
V : Type u
G : SimpleGraph V
hconn : G.Preconnected
u v : V
⊢ Nonempty (G.Walk u v)
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem to_mulShift_inj_of_isPrimitive {ψ : AddChar R R'} (hψ : IsPrimitive ψ) :
    Function.Injective ψ.mulShift

Proof state:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
⊢ Function.Injective ψ.mulShift

Tactic:
intro a b h

Result:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a = ψ.mulShift b
⊢ a = b

Proof state:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a * ψ.mulShift (-b) = ψ.mulShift b * ψ.mulShift (-b)
⊢ a = b

Tactic:
simp only [mulShift_mul, mulShift_zero, add_neg_cancel, mulShift_apply] at h

Result:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift (a + -b) = 1
⊢ a = b

Proof state:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a = ψ.mulShift b
⊢ a = b

Tactic:
apply_fun fun x => x * mulShift ψ (-b) at h

Result:
R : Type u
inst✝¹ : CommRing R
R' : Type v
inst✝ : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a * ψ.mulShift (-b) = ψ.mulShift b * ψ.mulShift (-b)
⊢ a = b
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem leftDistributor_hom_comp_biproduct_π {J : Type} [Fintype J] (X : C) (f : J → C) (j : J) :
    (leftDistributor X f).hom ≫ biproduct.π _ j = X ◁ biproduct.π _ j

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j => X ⊗ f j) j = X ◁ biproduct.π f j

Tactic:
classical
simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
X : C
f : J → C
j : J
⊢ (leftDistributor X f).hom ≫ biproduct.π (fun j => X ⊗ f j) j = X ◁ biproduct.π f j

Tactic:
simp [leftDistributor_hom, Preadditive.sum_comp, biproduct.ι_π, comp_dite]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_val (s) : volume s = StieltjesFunction.id.measure s

Proof state:
s : Set ℝ
⊢ volume s = StieltjesFunction.id.measure s

Tactic:
simp [volume_eq_stieltjes_id]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem norm_add (h : SameRay ℝ x y) : ‖x + y‖ = ‖x‖ + ‖y‖

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u + b • u‖ = ‖a • u‖ + ‖b • u‖

Tactic:
rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha,
  norm_smul_of_nonneg hb, add_mul]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoMod_inj {c : α} : toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]

Tactic:
simp_rw [toIcoMod_eq_toIcoMod, modEq_iff_eq_add_zsmul, sub_eq_iff_eq_add']

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma eventually_r_pos : ∀ᶠ (n : ℕ) in atTop, ∀ i, 0 < r i n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < r i x

Tactic:
exact fun i => (R.tendsto_atTop_r i).eventually_gt_atTop 0

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), 0 < r i n

Tactic:
rw [Filter.eventually_all]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, 0 < r i x